Elena Zucca -- Ciclo di lezioni per il Corso di MFI
Asserzioni alla Hoare
- Pagina del Corso di MFI
- Programma schematico del ciclo di lezioni: asserzioni
alla Hoare per un semplice linguaggio imperativo (ambiente fissato,
espressioni senza side-effects) di correttezza parziale e totale; sistema
di prova per i due casi; prova di soundness e correttezza del sistema di
prova; nozione di weakest precondition e di liberal weakest precondition;
esempi di prova di correttezza di algoritmi iterativi; cenni all'applicazione a linguaggi
object-oriented (Java Modeling Language).
- Testi di riferimento:
- COMPITINO 6 giugno testo
e
soluzioni
- COMPITINO 6 giugno voti
- Registro delle lezioni:
- Prima lezione (31 Marzo):
generalità su metodi di specifica;
introduzione informale delle asserzioni alla Hoare; asserzioni alla Hoare di correttezza parziale nell'approccio
estensionale; nozione di
weakest precondition di un comando rispetto ad una
postcondizione; weakest precondition per skip, assegnazione, concatenazione
e if-then-else.
- Seconda lezione (7 Aprile):
sistema di prova di Hoare di correttezza parziale; esempio di prova di un'asserzione
di correttezza parziale
per un ciclo while.
- Terza lezione (14 Aprile): prova di soundness del sistema di Hoare
per la correttezza parziale; esempio di prova di non terminazione di un
comando.
- Quarta lezione (28 Aprile): prova di completezza del sistema di
Hoare per la correttezza parziale; asserzioni alla Hoare di correttezza
totale; sistema di prova relativo.
- Quinta lezione (5 Maggio): Esempio di prova di terminazione di un ciclo
while ed altri esercizi.
- Sesta lezione (12 Maggio): Esempio della "bandiera nazionale
olandese"; prova di soundness e completezza del
sistema di Hoare per la correttezza totale (funzione di terminazione).
- Settima lezione (19 Maggio): cenni all'applicazione a linguaggi
object-oriented e a JML (Java Modeling Language): lucidi e home page di
JML (mi sembra che la cosa migliore da guardare sia questa documentazione).
- Ottava lezione (26 Maggio): Esercizi di preparazione al compitino.
Per esempi di soluzione di esercizi si veda:
Ritorno alla pagina precedente
Per suggerimenti e commenti si prega di scrivere a: Elena Zucca zucca@disi.unige.it
Ultima modifica: 26 Maggio 2003
|
|
