| | | 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. Viene anche presentata la semantica operazionale e la
semantica osservazionale di un linguaggio per la descrizione di
processi.
English Description
We introduce 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. Operational and observational semantics of a process
description language is also presented.
Programma
- Introduzione e sistemi di prova con regole di inferenza. (2h)
- Sintassi e semantica operazionale di un semplice linguaggio
imperativo (IMP). (4h)
- Domini e costruzioni di domini. (4h)
- Teorema del minimo punto fisso. (2h)
- Segnature e algebre dei termini. (2h)
- Semantica denotazionale di IMP. (2h)
- 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. (2h)
- Sintassi e semantica operazionale di un linguaggio perr la
descrizione di processi (CCS). (4h)
- Semantica osservazionale del CCS. (4h)
Ore lezione: | 30 | Ore esercitazione: | 10 | | | |
Bibliografia
- Glynn Winskel, "The formal Semantics of Programming Languages",
MIT Press, 1993. Capitoli: 1.3, 2, 3, 4, 5, 8, 11.
- Robin Milner, "Communication and Concurrency", Prentice Hall,
1989. Capitoli: 1-7, 10.
Modalità di esame
Scritto e orale