Metodi Formali dell'Informatica (IV anno) - a.a. 1998/99

Registro delle Lezioni

Le lezioni sono tenute da Moggi se non altrimenti specificato.
  1. 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).
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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).
  9. 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.
  10. 09/12/98 (Moggi). Esercizi di esame su specifiche.
  11. 11/12/98 (Moggi). Strutture applicative ed algebre combinatorie (parziali): assiomi equazionali, modelli sintattici ed operazionali, funzioni rappresentabili ed algoritmo di astrazione.
  12. 16/12/98 (Moggi). Esercizi su specifiche.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 29/01/98 (Moggi). Esercizi su CCS e LTS.

    PER LA SECONDA PARTE VEDI registro delle lezioni - ASD III anno