Metodi Formali dell'Informatica - a.a. 1997-98
Ultima modifica: 06 Aprile 1998.
Commenti a Eugenio Moggi.
L'esame si suddivide in una prova scritta ed una orale. La prova
scritta consiste di due parti valutate indipendentemente (una relativa
alla parte di corso tenuta da Astesiano, l'altra relativa a quella
tenuta da Moggi). Per ciascuna parte sara' dato un tempo prefissato
(in genere 2 ore). Durante lo scritto e' possibile consultare
dispense e libri.
E' possibile conservare il voto dello scritto (o anche di una delle 2
parti) negli appelli successivi, basta non ritentarlo (o non cosegnare
quella parte). La data degli orali viene concordata direttamente con
i docenti.
E' essenziale aver seguito i corsi di Logica Matematica e Linguaggi
di Programmazione.
- (Astesiano)
TIPI DI DATO ASTRATTI:
motivazione, formalizzazione, relazione con
linguaggi di programmazione (in particolare OO)
strutture eterogenee totali (algebre totali) del primo ordine con
eguaglianza: sintassi (segnatura,termini,formule del 1o ordine) e semantica
(modelli e semantica di termini e formule)
ADT come classe di strutture chiuse per isomorfismo (indipendenza dalla
rappresentazione)
- (Astesiano)
SPECIFICHE FORMALI:
motivazione, specifiche di requisiti (loose) e design (non-loose o
monomorfe, specifiche del primo ordine e condizionali (modello
iniziale), nozione di implementazione, consistenza e completezza
gerarchica, problema degli errori, cenno ad altri formalismi
(asserzioni alla Hoare)
- (Astesiano)
CONCETTI DI BASE PER PROCESSI REATTIVI E CONCORRENTI:
- linguaggio/modello a memoria condivisa (PARWHILE)
- sistemi di transizione etichettati:modello e sua motivazione, cenni a CCS
- specifiche di sistemi reattivi e concorrenti:cenni a logiche temporali
(requisiti) Labelled Transition Logic (design)
- cenni a paradigmi ulteriori:reti di Petri
- (Moggi)
FONDAMENTI DI PROGRAMMAZIONE FUNZIONALE E TIPI
- tipi funzionali
- lambda calcoli (tipati e non)
- polimorfismo (anche con accenni ai linguaggi OO)
- valutazione simbolica: sistemi di riscrittura per CL e lambda-calcolo
- (Moggi)
MODELLI DI CALCOLO: TM, RAM, funzioni calcolabili, complessita' tempo
e spazio, relazione tra i due modelli di calcolo, Tesi di Church e
Tesi di Church estesa.
- (Moggi)
CALCOLABILITA': funzioni calcolabili, problemi/sottoinsiemi decidibili
e semidecidibili, riducibilita' tra problemi, codifica delle TM, TM
universale, esempi di problemi non (semi)decidibili, proprieta' di
chiusura dei sottoinsiemi (semi)decidibili.
- (Moggi)
COMPLESSITA': classi di complessita', relazioni tra classi di
complessita' ed O-notazione, classi naturali di complessita' (P, NP),
teorema di Cook, esempi di problemi NP-completi.
- (Moggi)
PANORAMICA SU ALTRI ARGOMENTI DI COMPLESSITA": accenni ad altri
modelli di calcolo (per algoritmi probabilistici e paralleli), e
relative classi di complessita'.
-
[HS] J.R. Hindley, J.P. Seldin, "Introduction to Combinators and
Lambda-Calculus". Cambridge University Press. 1986.
(Solo i capitoli 1, 2, 3, 6, 7, 8, 9, 10)
-
[CW] L. Cardelli, P. Wegner, "On Understanding Types, Data
Abstraction, and Polymorphism". Computing Surveys, vol. 17, n. 4, 1985.
(Tutto)
-
[P] C. Papadimitriou, "Computational Complexity". Addision-Wesley.
1994.
(Solo i capitoli 1, 2, 3, 7, 8, 9)
-
E. Moggi, Note 1-4