ECTS - University of Pisa
| Modules | Area | Type | Hours | Teacher(s) | |
| MODELLI DI CALCOLO | INF/01 | LEZIONI | 72 |
|
Gli studenti dovranno acquisire solide basi di conoscenza circa i principi della semantica operazionale e denotazionale, le tecniche per relazionare l'una con l'altra nel caso di linguaggi imperativi e funzionali di ordine superiore. Inoltre dovranno familiarizzare con i principi della semantica operazionale e astratta per algebra di processi concorrenti, con le principali logiche temporali e modali (HM, LTL, CTL*, mu-calculus) usate per esprimere proprietà di tali processi e con modelli operazionali con probabilità. Gli ultimi saranno studiati dal punto di vista degli automi probabilistici e stocastici, delle catene di Markov e dal linguaggio di modellazione PEPA.
Students are expected to acquire solid knowledge about the principles of operational semantics, the principles of denotational semantics, and the techniques to relate one to the other for an imperative language and for a higher order functional language. Moreover, they will acquire some knowledge about the operational and observational semantics of two process description languages (CCS and pi-calculus), about temporal and modal logics (HM, LTL, CTL*, mu-calculus) and operational nondeterministic models with discrete probabilities. The latter are presented from the perspective of probabilistic and stochastic automata, and of the PEPA calculus.
In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione e/o progetti software individuali.
L'esame scritto servirà a verificare che gli studenti abbiano compreso il materiale presentato durante il corso e che siano in grado di organizzare e strutturare i concetti appresi in efficaci risposte scritte.
Durante l'esame orale gli studenti dovranno dimostrare di aver compreso gli aspetti più concettuali e di essere in grado di argomentare le risposte con proprietà di linguaggio usando i termini corretti.
Metodi di verifica:
Informazione aggiuntiva:
La valutazione sarà basata su esami scritti e orale. L'esame scritto finale non sarà necessario se i compitini saranno valutati positivamente.
In case of virtual lectures, written exams will be replaced by self-assessment tests and/or individual software projects.
In the written exam the student must demonstrate his/her knowledge of the course material and to organise an effective and correctly written reply. During the oral exam the student must be able to demonstrate his/her knowledge of the course material and be able to discuss the reading matter thoughtfully and with propriety of expression.
Methods:
Further information:
The evaluation will be based on written and oral exams. The written exam is not necessary if the mid-terms exams are evaluated positively.
Al termine del corso gli studenti dovrebbero essere in grado di dimostrare semplici proprietà formali di linguaggi e sistemi imperativi, dichiarativi, concorrenti e probabilistici. In particolare dovrebbero essere in grado di applicare correttamente i più comuni principi di induzione e la teoria del punto fisso.
At the end of the course the student should be able to state and prove formal properties of imperative, declaratice, concurrent and probabilistic systems. In particular, they should be able to apply several induction principles and fixpoint theory.
Il corso comprende test di auto-valutazione e/o progetti software individuali.
L'esame orale verte principalmente sulle definizioni e sulle proprietà mostrate nel corso, incluse le dimostrazioni dei risultati principali e può includere lo svolgimento di esercizi analoghi a quelli visti a lezione.
The course includes self-assessment tests and/or individual software projects.
The oral exam focuses on the definitions and properties presented in the course and can include written exercises analogous to the ones presented during classrooms.
Alla fine del corso gli studenti dovrebbero essere in grado di comprendere e applicare sistemi logici e definizioni induttive, di definire la semantica di linguaggi di programmazione, e di ragionare su eventuali equivalenze e corrispondenze tra specifiche astratte.
At the end of the course the student should be able to understand logic systems and inductive definitions, to assign semantics to programs, to reason about program equivalence and compliance to abstract specifications.
Esame orale.
Test di auto-valutazione e/o progetti software individuali.
Written and oral exam.
Self-assessment tests and/or individual software projects.
Non ci sono prerequisiti stringenti, ma ci si aspetta che gli studenti abbiano una buona familiarità con la matematica discreta, con le formule logiche del prim'ordine, con le grammatiche libere da contesto e siano in grado di comprendere frammenti di codice scritti in linguaggi imperativi e funzionali.
There are no prerequisites, but the students are expected to have some familiarity with discrete mathematics, first-order logic formulas, context-free grammars, and code fragments in imperative and functional style.
Lezioni frontali e esercitazioni collettive.
Attività di apprendimento:
Frequenza: fortemente consigliata
Delivery: face to face
Learning activities:
Attendance: Advised
Teaching methods:
Introduzione di cinque modelli computazionali differenti e studio delle loro proprietà formali principali (imperativo: IMP, funzionale: HOFL, processi concorrenti: CCS, calcoli con nomi: pi-calculus, sistemi probabilistici e stocastici: Segala automata e PEPA) accompagnati da principi di induzione e da metodi di dimostrazione.
The introduction of five different computational models (imperative: IMP, functional: HOFL, processes: CCS, nominal: pi-calculus, probabilistic and stochastic: Segala automata and PEPA) together with induction principles and formal proof methods.
Testo principale:
Letture opzionali consigliate:
Main text:
Other readings:
Nessuna variazione.
No variation.
Il corso comprende test di auto-valutazione e/o progetti software individuali.
L'esame orale verte principalmente sulle definizioni e sulle proprietà mostrate nel corso, incluse le dimostrazioni dei risultati principali e può includere lo svolgimento di esercizi analoghi a quelli visti a lezione.
The course includes self-assessment tests and/or individual software projects.
The oral exam focuses on the definitions and properties presented in the course and can include written exercises analogous to the ones presented during classrooms.
http://didawiki.di.unipi.it/doku.php/magistraleinformatica/psc/
Alcuni strumenti presentati nel corso:
Some teaching tools overviewed in the course are:
Nessuna
None
