Topic outline
-
-
Le lezioni di questo modulo cominceranno lunedì 3 ottobre 2022. Le lezioni si tengono il lunedì e il giovedì dalle 15:30 alle 18:30, ma in alcune date termineranno alle 17:30. Le lezioni saranno esclusivamente in presenza; quando possibile, il materiale relativo a una lezione sarà pubblicato in anticipo. Saranno anche disponibili le registrazioni delle lezioni dell'anno scorso sugli stessi argomenti.
Questo è il calendario delle prime lezioni, dedicate alle tecniche di dimostrazioni di correttezza di programmi e alla logica di Hoare. Consultate sempre il sito per eventuali variazioni.
- 3 ottobre, 15:30-18:30, aula U4-02
- 6 ottobre, 15:30-17:30, aula U24-C1
- 10 ottobre, 15:30-18:30, aula U4-02
- 13 ottobre, 15:30-18:30, aula U24-C1
- 17 ottobre, 15:30-17:30, aula U4-02
Calendario delle lezioni dedicate ai modelli di sistemi concorrenti: CCS- 20 ottobre, 15:30-18:30, aula U24-C1
- 24 ottobre, 15:30-17:30, aula U4-02
- 27 ottobre, 15:30-16:30, aula U24-C1
- 3 novembre, 15:30-18:30, aula U24-C1
- 7 novembre, 15:30-18:30, aula U4-02
- 10 novembre, 15:30-18:30, aula U24-C1
- 14 novembre, 15:30-18:30, aula U4-02
Calendario delle lezioni dedicate ai modelli di sistemi concorrenti: reti di Petri- 17 novembre, 15:30-18:30, aula U24-C1
- 21 novembre, 15:30-18:30, aula U4-02
- 24 novembre, 15:30-18:30, aula U24-C1
- 28 novembre, 15:30-18:30, aula U4-021
- 1 dicembre, 15:30-18:30, aula U24-C1
Calendario delle lezioni su logiche temporali e model-checking (consultate sempre il sito per eventuali variazioni)- 5 dicembre 15:30-17:30, aula U4-02
- 12 dicembre 15:30-17:30, aula U4-02
- 15 dicembre 15:30-17:30, aula U24-C1
- 19 dicembre 15:30-17:30, aula U4-02
- 22 dicembre 15:30-17:30, aula U24-C1
- 9 gennaio 15:30-17:30, aula U4-02
In preparazione all'esame, si potranno tenere incontri supplementari -
La prova scritta comprende quattro esercizi, uno per ciascuno dei seguenti argomenti:
- CCS e bisimulazione
- Reti di Petri e processi
- Dimostrazioni di correttezza con la logica di Hoare
- Logiche temporali e model-checking
-
Reservation
Gli studenti che intendono sostenere la prova del modulo Modelli della concorrenza nell'appello del 13 giugno 2023 sono pregati di compilare questo modulo entro il 10 giugno. Chi prevede di completare l'esame dell'insegnamento Modelli e computabilità in questo appello deve anche iscriversi all'esame sul sito delle segreterie online.
-
Reservation
Gli studenti che intendono sostenere la prova del modulo Modelli della concorrenza nell'appello del 4 luglio 2023 sono pregati di compilare questo modulo entro il 30 giugno. Solo chi prevede di completare l'esame dell'insegnamento Modelli e computabilità in questo appello deve anche iscriversi all'esame sul sito delle segreterie online.
-
Reservation
Gli studenti che intendono sostenere la prova del modulo Modelli della concorrenza nell'appello dell'11 settembre 2023 sono pregati di compilare questo modulo entro l'8 settembre. Solo chi prevede di completare l'esame dell'insegnamento Modelli e computabilità in questo appello deve anche iscriversi all'esame sul sito delle segreterie online.
-
Come si può stabilire se un programma è "corretto"? In questa parte del corso si studia un metodo rigoroso per esprimere i requisiti di programmi sequenziali e per dimostrare che un programma soddisfa un requisito assegnato. Lo strumento fondamentale è la logica di Hoare, definita a partire dalla logica proposizionale e dei predicati.
-
15:30-18:30, aula U4-02
Riassunto della lezione- Introduzione generale al modulo (vedi Introduzione)
- Esempio di dimostrazione di correttezza informale (vedi Dimostrazione informale)
- Nozioni fondamentali di logica proposizionale, prima parte (vedi Logica proposizionale)
-
15:30-17:30, aula U24-C1
Il materiale di consultazione non è ancora completo.
Riassunto
- Ripasso di logica proposizionale, seconda parte (vedi Logica proposizionale nel materiale della prima lezione)
- Una logica per ragionare su programmi: le triple di Hoare
- Definizione di un linguaggio di programmazione
- Regole di derivazione della logica di Hoare, prima parte (vedi Logica di Hoare, prima parte; attenzione: nella definizione delle espressioni aritmetiche manca la clausola che dice che ogni nome di variabile è un'espressione aritmetica)
-
15:30-17:30, aula U4-02
Riassunto della lezione
- Regole di derivazione della logica di Hoare, seconda parte
- La regola delle istruzioni iterative: definizione di invariante di ciclo
- Distinzione fra correttezza parziale e correttezza totale
- Esercizi
-
15:30-18:30, aula U24C1
Il contenuto di questa cartella verrà arricchito nei prossimi giorni.
Riassunto
- Logica di Hoare: la regola di derivazione per la correttezza totale di istruzioni iterative
- Considerazioni su correttezza e completezza della logica di Hoare
- Precondizione più debole (weakest precondition): definizione, significato intuitivo, esempi
- Corrispondenza fra stati e formule
-
15:30-17:30, aula U4-02
Riassunto
- Programmi come trasformatori di stato; computazione come cammino in un grafo
- Schema generale di una dimostrazione di correttezza
- La logica di Hoare nella pratica: design by contract, Eiffel, Java Modeling language
- La logica di Hoare come fondamento di una semantica dei programmi
- Esercizi
Attenzione: nel diagramma a pagina 7 del file mdc-finale.pdf la regione associata alla formula "s" dovrebbe contenere tutti gli stati nell'intersezione di "i" e "non B".
-
Presentiamo un linguaggio (CCS - Calculus of Communicating Systems) con il quale è possibile specificare, in forma astratta, sistemi concorrenti, cioè formati da componenti che interagiscono. Studiamo una nozione di equivalenza fra "programmi" scritti in questo linguaggio, e il suo interesse, sia teorico sia applicativo.
-
Questi esercizi verranno corretti lunedì 14 novembre.
-
Per la verifica della bisimulazione con la tecnica tratta dalla teoria dei giochi dell'"attaccante e difensore" si veda anche la sezione 3.5 e 3.5.1 del testo "Reactive Systems" al link precedente. (Si noti che viene presentata la tecnica per la Bisimulazione forte e solo nella sezione 3.5.1 quella per la Bisimulazione debole.)
-
File
Caal è un tool open source sviluppato presso l'Università di Aalborg, in Danimarca e disponibile al link: https://caal.cs.aau.dk/. Consiste di vari moduli tra cui un editor per CCS, uno per la visualizzazione dei processi, uno per la verifica delle equivalenze e il model checking e uno per il gioco della bisimulazione. Questo file presenta gli aspetti fondamentali del tool e contiene indicazioni su come utilizzarlo.
-
Le reti di Petri costituiscono un modello formale per rappresentare sistemi distribuiti e processi concorrenti a partire dalla nozione di stato locale. Studiamo i fondamenti della teoria delle reti di Petri, e alcune tecniche per analizzarne le caratteristiche.
-
questi esercizi sui processi non sequenziali verranno corretti il 1 dicembre
-
Di questo articolo si considerino in particolare (senza le dimostrazioni) le seguenti sezioni:
- sez 1, 2, 3
- 4.1 (fino al teorema 29 compreso), 4.5
- 5, 5.1, 5.2, 5.3, sui processi non sequenziali si vedano anche le slide pubblicate. -
articolo su Elementary net systems e processi non sequenziali
-
Articolo su una panoramica della teoria e delle applicazioni delle Reti di Petri
-
articolo sui fondamenti della teoria delle reti di Petri
-
Fissato un modello formale di un sistema, reale o da realizzare, vogliamo stabilire se il modello soddisfa certi requisiti. Le tecniche di model-checking si basano sull'impiego di logiche modali e temporali per esprimere le proprietà che vogliamo studiare, e su algoritmi che decidono se il modello del sistema in esame le soddisfa o no. Studiamo alcuni linguaggi logici e i relativi algoritmi di decisione.
-
Raccomando di leggere questo breve articolo introduttivo, sorvolando in prima lettura sui dettagli dell'esempio nella sezione 3, e tenendo conto che nella descrizione degli operatori di logica temporale ci sono alcuni errori (nel corso delle lezioni e negli appunti pubblicati sul sito verranno date le definizioni formali precise).
-
Riferimenti a materiale di consultazione
-
Da leggere: paragrafo 1 (Introduction), introduzione alla sezione 3 (Systems and Properties), sezione 3.1 (Transition Systems), sezione 3.2 (Properties and Temporal Logic).
-
Glynn Winskel
Per i teoremi di punto fisso, si veda la sezione 1.5.
-
Clarke, Emerson, Sifakis
Turing Lecture
-
Attenzione: il contenuto è provvisorio; ci sono ripetizioni e contenuti in ordine diverso rispetto alla lezione. I file saranno aggiornati il prima possibile.
-
di HA Priestley, tratto da R. Backhouse et al. (Eds.): Algebraic and Coalgebraic Methods . . . , LNCS 2297, pp. 21–78, 2002. Springer-Verlag.
-
Kaltura Video Resource
15:30-17:30, aula U4-02
Il livello della registrazione audio è molto basso; provate a regolare al massimo il volume di uscita.
-
Kaltura Video Resource
15:30-17:30, aula U4-02
Il livello della registrazione audio è molto basso; provate a regolare al massimo il volume di uscita.
-