| | | corso | | | | |
Tecniche di specifica e dimostrazione
Codice: | AA031 | Crediti: | 6 | Semestre: | 2 | Sigla: | TSD | |
|
Settore disciplinare: | INF/01 - Informatica |
Docente
Ugo Montanari
Tel. 0502212721Prerequisiti
Elementi di Programmazione
Elementi di Logica
Obiettivi di apprendimento
La definizione formale di semplici linguaggi di programmazione.
Descrizione
Il corso presenta i principi della semantica
operazionale, i principi della semantica denotazionale e le tecniche per
confrontarle nel caso di un linguaggio imperativo e di un linguaggio
funzionale di ordine superiore.
English Description
We will present the principles of operational semantics,
the principles of denotational semantics, and the techniques to relate one
to the other for an imperative language, and for a higher order functional
language.
Programma
- Introduzione e sistemi di prova con regole di inferenza. (2h)
- Sintassi e semantica operazionale di un semplice linguaggio imperativo
(IMP). (6h)
- Domini e costruzioni di domini. (6h)
- Teorema del minimo punto fisso. (2h)
- Segnature e algebre dei termini. (2h)
- Semantica denotazionale di IMP. (4h)
- Tecniche di prova per induzione. (4h)
- Equivalenza tra semantica operazionale e denotazionale di IMP. (4h)
- Sintassi e semantica operazionale lazy di un linguaggio funzionale higher
order (HOL). (4h)
- Semantica denotazionale lazy di HOL. (2h)
- Relazione tra semantica operazionale e denotazionale di HOL. (4h)
Bibliografia
Glynn Winskel, "The formal Semantics of Programming
Languages", MIT Press, 1993. Capitoli: 1.3, 2, 3, 4, 5, 8, 11.
Modalità di esame
Scritto e orale