Programmazione: Laboratorio di Tecniche di Raffinamento

Carlo Montangero      Tel. 0502212799

Programmazione e Logica

Il corso si propone di sviluppare competenze nella produzione sistematica di programmi sequenziali con tecniche di raffinamento formale.

Verranno trattati i metodi di raffinamento dei programmi e dei dati, che permettono di ottenere versioni efficienti in spazio e ottimizzate in tempo di programmi progettati in termini di dati astratti. Un tipico esempio è la derivazione della versione iterativa con spazio costante di quick sort. L'approccio seguito è dovuto a C.Morgan, e permette di documentare sistematicamernte le scelte di progetto, al fine di soddisfare uno dei requisiti fondamentali dello sviluppo professionale di software. Si tratta di un laboratorio, perchè ci sarà poca teoria e molti esempi.

We present program and data refinemement in the style due to C. Morgan. The approach is practical, with more examples than theory.

1. Programmi come contratti, raffinamento: Programmi astratti, concreti e misti 2. Un'estensione del linguaggio dei guarded commands: Tipi, dichiarazioni, procedure e moduli 3. Trasformazioni di stato e raffinamento di dati: Aggiunta e eliminazione di variabili, funzioni di astrazione 4. Studio di casi

C. Morgan. "Programming from specifications" Prentice Hall, 1994 (seconda edizione).

Scritto e orale