Programmazione: Metodi Formali

Salvatore Ruggieri      Tel. 0502212782

Fondamenti dell'Informatica: Semantica

L'enfasi è sull'uso pratico dei metodi formali nella dimostrazione di proprietà di programmi sequenziali e paralleli (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.

Il corso presenta l'uso del sistema di prova basato sulle triple di Hoare per la dimostrazione di proprietà di programmi scritti in linguaggi di crescente complessità. Si inizia con un semplice linguaggio imperativo deterministico e poi si passa a trattare il parallelismo prima in un linguaggio con processi paralleli disgiunti, poi in un linguaggio in cui i processi condividono variabili e, infine, in un linguaggio arricchito con primitive di sincronizzazione.

The emphasis is on the practical use of formal methods in proving properties of sequential and parallel 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 prove correctness and termination of languages of increasing complexity: a deterministic sequential language, a language allowing disjoint parallel programs, a language allowing shared variables among parallel programs, and a language allowing also synchronization among programs.

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, programmazione funzionale e ragionamento equazionale (4h)

Programmazione imperativa sequenziale deterministica: sintassi, semantica operazionale, teoria della dimostrazione, teorema di correttezza, studio di casi (6h)

Programmazione imperativa a parallelismo disgiunto: sintassi, semantica operazionale, teoria della dimostrazione, studio di casi (4h)

Programmazione imperativa parallela con condivisione di variabili : sintassi, semantica operazionale, teoria della dimostrazione, studio di casi (5h)

Programmazione parallela con sincronizzazione : sintassi, semantica operazionale, teoria della dimostrazione, studio di casi (7h)

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