Programma del corso di Metodi Formali
dell'Informatica
a.a. 2001/2002
Tema centrale del corso sono gli strumenti per la comprensione esatta di programmi
Il corso si articola in due parti centrate la prima sulla semantica dei
linguaggi di programmazione e la seconda sulle tecniche di specifica per
linguaggi imperativi e per tipi di dato.
Semantica di linguaggi
Le seguenti tecniche verranno inizialmente illustrate su (versioni
semplificate di) un linguaggio imperativo didattico.
- Semantica statica
- Semantica dinamica in stile denotazionale algebrico
- Semantica dinamica in stile operazionale strutturale sia a grandi che a
piccoli passi
Applicando le tecniche viste nel caso imperativo, con le dovute modifiche,
si studierà inoltre un linguaggio applicativo con tipi d'ordine superiore.
Lambda Calcolo
Nozione base di applicazione, semplificazione, alfa e beta regole per il
lambda calcolo puro.
Problematiche poste dal tipo s = (s ->s)
Concorrenza
- Modelli per la concorrenza basati su memoria condivisa e su scambio di
messaggi.
- Linguaggi per tali paradigmi: ParWhile e CCS
- Nozione di bisimulazione e bisimuazione forte
- Alberi di transizione e di sincornizzazione
Specifiche
Asserzioni per linguaggi imperativi
Nozione base di asserzione, validità debole e forte.
Sistema di Hoare
Specifiche Algebriche
Nozione base di segnatura, formula, algebra parziale, validità e
modelli.
Modelli iniziali, caratterizzazione e condizioni sufficienti per l'esistenza.
Sistema di Birkhoff con trattamento esplicito/implicito della
quantificazione.
CASL
Il Common Algebraic Specification Language:
construtti base.
Semantica di CASL.