Unità didattica
Titolo del corso
Modelli della Concorrenza
Codice identificativo del corso
2223-1-F1801Q132-F1801Q132M
Schema della sezione
-
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.
-
-
Cartella
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)
-
Cartella
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)
-
Cartella
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
-
Cartella
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
-
-
Cartella
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".
-