Le lezioni sono tenute da Moggi se non altrimenti specificato.
06/11/98 (Moggi).
Introduzione al corso.
Discussione su qualita' del SW, fattori qualitativi esterni ed
interni, documentazione e manutenzione del SW.
Tipi di dato astratti, desiderata per formalismi/metodologie di
specifica. Astrazione, information hiding, interfacce e approccio
modulare.
Algebre con predicati (strutture del primo ordine) many-sorted:
segnatura, algebra, termini, interpretazione dei termini, omomorfismo
di algebre, omomorfismo di segnature (funzione da simboli a simboli).
11/11/98 (Moggi).
Interpretazione di termini e formule, e varie nozioni di
soddisfacibilita'. Modelli di una specifica e teoria di una classe di
strutture del primo ordine.
La nozione di categoria ed esempi. La categoria Sig delle segnature,
e la categoria delle algebre (per una segnatura). Nozioni
categoriali: mono, epi, iso. Invarianza della soddisfacibilita' di
formule per iso (se non vi sono predicati un omomorfismo e' iso sse e'
epi e mono). Semantica di una "specifica" come classe di strutture
del primo ordine chiusa per iso.
13/11/98 (Moggi).
Isomorfismi, omomorfismi, strong omomorfismi e soddisfacibilita'.
Nozioni categoriali: oggetto iniziale, unicita' a meno di iso.
L'algebra dei termini con variabili in X, e sua proprieta'
"universale". Algebra iniziale come algebra dei termini.
Algebre term-generated, definizione sintattica, e definizione
semantica in termini di sottoalgebre.
18/11/98 (Moggi).
Costruzione di un modello iniziale term-generated per una classe C di
algebre. Verita' minima e caratterizzazione dei modelli iniziali e
term-generated. Esempi di specifiche che ammettono o non ammettono
modello iniziale.
20/11/98 (Moggi).
Sistemi deduttivi, soundness e completeness relative ad un frammento.
Il problema dei carrier vuoti. Specifiche condizionali, sistema di
Birkhoff e variante ristretta alle formule atomiche. Completezza del
sistema di Birkhoff, esistenza del modello iniziale per specifiche
condizionali.
25/11/98 (Moggi).
Metalinguaggio per specifiche strutturare e sua semantica. Esempi di
operazioni su specifiche. Specifica gerarchica e relazioni tra parte
primitiva ed estensione. Raffinamento di specifiche e la relazione di
implementazione. Monotonia delle operazioni rispetto alla relazione
di implementazione.
27/11/98 (Moggi).
Sistemi di riscrittura: relazione di riscrittura e relazioni derivate,
coppia usabile, forma normale, confluenza e terminazione. Teorema di
esistenza/unicita' delle forme normali per un sistema di riscrittura
terminante/confluente. Relazioni tra riscrittura e teoria equazionale
in generale e nella ipotesi di sistema confluente.
02/12/98 (Moggi).
Caratterizzazione e decidibilita' della teoria equazionale nella
ipotesi di sistema terminante e confluente. Il modello iniziale delle
forme normali. Esempi di sistemi di riscrittura. Espressioni
aritmetiche sui naturali, logical combinatoria e operatore di punto
fisso, linguaggio per composizione sequenziale.
Tecnica per dimostrare la terminazione mediante una misura a valori in
un ordine parziale ben fondato.
Le nozioni di coppia critica e confluenza locale. Teorema di Newman
(terminazione e confluenza locale implicano confluenza) e di
Knuth-Bendix (tutte le coppie critiche sono confluenti implica
confluenza).
04/12/98 (Moggi).
I sistemi ortogonali (cioe' left-linear e senza coppie critiche),
ortogonalita' implica confluenza, confluenza e terminazione debole
implicano decidibilita' (se il sistema e' effettivo) e modello
iniziale delle forme normali.
Esempio di studio del modello iniziale mediante tecniche di
riscrittura.
09/12/98 (Moggi).
Esercizi di esame su specifiche.
11/12/98 (Moggi).
Strutture applicative ed algebre combinatorie (parziali): assiomi
equazionali, modelli sintattici ed operazionali, funzioni
rappresentabili ed algoritmo di astrazione.
16/12/98 (Moggi).
Esercizi su specifiche.
18/12/98 (Moggi).
Estensioni della logica combinatoria: estensionalita', combinatore di
scelta dei rappresentanti canonici, test di uguaglianza.
Codifica di tipi di dato in una algebra combinatoria: booleani,
naturali, coppie.
08/01/98 (Moggi).
Operatori di punto fisso e rappresentazione delle funzioni parziali
ricorsive il logical combinatoria (indecidibilita').
Lambda calcolo, sintassi, variabili libere e sostituzione con
ridenominazione delle variabili legate, alfa- e beta-conversione.
Analogie con le teorie equazioni e complicazioni tecniche legate
alla necessita' di lavorare a meno di alfa-conversione. Proprieta' CR
per il lambda-calcolo.
Corrispondenza tra lambda-calcolo con beta-conversione e logica
combinatoria con operatore di scelta del rappresentante canonico.
13/01/98 (Moggi).
Struttura applicativa parziale indotto da una semantica operazionale.
Osservazioni sui programmi, equivalenza osservazionale e struttura
applicativa parziale quoziente, soundness di teorie equazionali
rispetto all'algebra quoziente.
Semantica operazionale con errore, Sistemi di tipi [C97] e check
statico degli errori. Semantica dei tipi in una struttura applicativa
parziale: sottoinsiemi, quozienti parziali.
Estensioni del lambda calcolo tipato semplice: tipi record e tipi
variante.
15/01/98 (Moggi).
Subject Reduction come Relazione tra type systems e semantica
operazionale (con errore).
Type systems con variabili di tipo, sub-typing (tipi record fissi e
record estendibili), tipi polimorfi, astratti, ricorsivi e references.
20/01/98 (Moggi).
Modalita' di interazione tra processi concorrenti. Label Transition
Systems (LTS) ed esempi di descrizione sistemi interattivi. Il CCS
come formalismo per descrivere sistemi concorrenti e paralleli,
costrutti dinamici e statici. Semantica operazione del CCS ed LTS dei
processi (cioe' espressioni chiuse) CCS.
Esempi di sistemi descritti mediante il CCS: cella, buffer di
capacita' limitata ed illimitata, implementazione di buffer di
capacita' k componendo buffer di capacita' 1.
22/01/98 (Moggi).
Equivalenze per LTS e processi CCS: trace equivalence (identifica
troppo), strong bisimulation (distingue troppo), esempi. Relazione di
bisimulazione, e tecnica per dimostrare che due processi sono strong
bisimilar. Proprieta' della strong bisimulation: congruenza,
proprieta' equazione della scelta non deterministica e della
composizione parallele, teorema di espansione.
Alberi di sincronizzazione (definizione induttiva) e rappresentati
canonici delle classi di equivalenza modulo strong bisimulation.
27/01/98 (Moggi).
La bisimulazione debole (weak bisimulation) e la congruenza indotta
(weak congruence): definizioni alternative.
L'alternating bit protocol: forlamizzazione mediante LTS (o in CCS),
correttezza del protocollo mediante la costruzione di una relazione di
bisimulazione debole.