Programmazione: Metodi Formali

Salvatore Ruggieri      Tel. 0502212782

L'enfasi è sull'uso pratico dei metodi formali nella dimostrazione di proprietà di programmi sequenziali deterministici e nondeterministici (terminazione, correttezza, equivalenza), nella sintesi di programmi corretti, nella trasformazione e ottimizzazione di programmi. Il corso si propone quindi di discutere gli aspetti metodologici e la applicabilità dei metodi formali alla programmazione, su piccola/media scala, di algoritmi significativi.

Il corso presenta il sistema di prova basato sulle triple di Hoare per la dimostrazione di proprietà di programmi sequenziali deterministici e nondeterministici. Verranno studiate le metodologie di sviluppo sistematico di programmi a partire dalla loro specifica ed applicate a casi di studio significativi, quali algoritmi di ordinamento, costruzione di alberi di decisione, algoritmi di clustering.

The emphasis is on the practical use of formal methods in proving properties of sequential deterministic and nondeterministic programs (termination, correctness, equivalence). The aim is to discuss the methodological aspects and the applicability of formal methods to small/medium scale programming.

The main topic is the use of Hoarès Proof Systems to reason about correctness and termination of deterministic and nondeterministic programs. The course presents the methodologies of systematic program development and applications of them to significative case studies, such as sorting, decision tree construction, clustering algorithms.

Introduzione: il ruolo dei metodi formali nella programmazione, il problema della correttezza, verifica sintesi e trasformazione, metodo e formato di dimostrazione, programmazione imperativa e triple di Hoare. Test di pre e postcondizioni in Java. Esercitazione (8h)

Programmazione sequenziale deterministica: sintassi, semantica operazionale, teoria della dimostrazione, teorema di correttezza. Studio di casi: the Minimum-Sum Section Problem. Esercitazione (10h)

Programmazione sequenziale nondeterministica: sintassi, semantica operazionale, teoria della dimostrazione. Assegnamento random e cenni sulla fairness. Simulazione del nondeterminismo in Java. Studio di casi: the Welfare Crook Problem. Esercitazione (10h)

Analisi di algoritmi : algoritmi di ordinamento (4h), costruzione di alberi di decisione (4h), algoritmi di clustering (4h)

K.R.Apt and E.Olderog "Verification of sequential and concurrent programs", Second Edition Springer-Verlag 1997

Dispense ed articoli distribuiti dal docente.

Scritto e orale