Tecniche di specifica e dimostrazione

Ugo Montanari      Tel. 0502212721

Elementi di Programmazione
Elementi di Logica

La definizione formale di semplici linguaggi di programmazione.

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.

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.

• 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)

• 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.

Scritto e orale