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.
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 consiste di esercizi che richiedono l'applicazione di tecniche formali di prova ad alcuni casi specifici accuratamente selezionati.
L'esame orale verte principalmente sulle definizioni e sulle proprietà mostrate nel corso, incluse le dimostrazioni dei risultati principali.
In case of virtual lectures, written exams will be replaced by self-assessment tests and/or individual software projects.
The written exam consists of exercises that require to apply formal analysis techniques to some carefully chosen cases.
The oral exam focuses on the definitions and properties presented in the course.
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 scritto e orale.
In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione e/o progetti software individuali.
Written and oral exam.
In case of virtual lectures, written exams will be replaced by 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.
In caso di didattica a distanza, gli esami scritti potranno essere sostituiti da test di auto-valutazione e/o progetti software individuali.
Esame scritto (due compitini o un esame finale) e esame orale.
L'esame scritto consiste di una serie di esercizi da risolvere in 2 ore. Ogni esercizio ha un punteggio assegnato e il voto finale è la somma dei punteggi conseguiti sui singoli esercizi. I testi delle sessioni di esame precedenti sono raggiungibili dalla pagina del corso.
L'esame orale prende spunto dalla discussione dell'esame scritto per poi affrontare gli argomenti principali presentati durante il corso. La durata tipica dell'esame orale è 30'/40'.
Avviso:
A causa dell'emergenza COVID-19, a partire dall'appello di giugno 2020 e fino a nuovo avviso le modalità di esame vengono modificate nella sola prova orale, in modo da permette agli studenti di sostenere l'esame a distanza.
In case of virtual lectures, written exams will be replaced by self-assessment tests and/or individual software projects.
Written (two mid-term, or one regular) exam and oral exam.
The written exam consists of a series of exercises to be solved in 2 hours. Each exercise is assigned some score and the overal score is the sum of scores for each exercise. The texts of exams from previous sessions and academic years are linked from the web page of the course.
The oral exam can involve the discussion of the written exam as well as questions about the main topics of the course topics. The average duration of the oral exam is 30'/40'
Notice:
Due to the COVID-19 countermeasures, for the current period, the evaluation will be solely based on oral exams.
Alcuni strumenti presentati nel corso:
Some teaching tools overviewed in the course are:
None
