Docente: Alberto
Pettorossi.
Tuesday 11:30-13:15 (Room 12)
Wednesday 10:30-12:15 (Room 12)
Friday
09:30-11:15 (Room 12)
Lectures: from 10.12.02 to 14.02.03.
Exams: 20.02.03 10:00 am (Room 10)
You can talk to the teacher after the lectures or by appointment.
Obiettivo del corso. Il corso
si
propone di offrire una panoramica dei metodi
per la definizione della semantica dei linguaggi di programmazione
imperativi,
funzionali, logici, concorrenti e a oggetti. Tali metodi
consentono
di
approfondire la comprensione logica e algebrica delle varie tecniche
esistenti
per la specifica e la verifica di proprietà dei programmi
scritti in tali
linguaggi. L'approfondimento teorico verrà consolidato dall'uso
e dallo
sviluppo di strumenti software opportuni.
Esami: martedi`
09.09.03
ore 10 aula 12. ***
martedi` 23.09.03 ore 10 aula 12. ***
*** Occorre fare la prenotazione nel foglio
predisposto
all'ingresso di Ingegneria dell'Informazione.
Programma
d'esame con informazioni bibliografiche.
Take-home
exam.
Programma del corso:
1. Decidability and Turing computability. Partial Recursive
Functions.
2. Structural induction, well-founded induction, and rule
induction.
Recursion Theorem.
3. Operational, denotational, and axiomatic semantics of an
imperative language.
Hoare's triples for partial correctness. Hoare's
calculus: soundness and relative completeness.
4. Operational and denotational semantics of a first order
functional
language:
call-by-value and call-by-name regimes.
5. Domain theory. A metalanguage for denotational semantics.
Bekic's Theorem.
Inclusive predicates and proofs of properties of
functional programs.
6. Operational and denotational semantics of a higher order
functional language: eager semantics
and lazy semantics. Fixpoint operators. Beta and
eta rules. Adequacy and full abstraction.
7. Operational and denotational semantics of Horn-clause
programs.
8. Dijkstra's nondeterministic guarded commands. Owicki-Gries
rules for parallel commands.
Milner's calculus for communicating concurrent
processes.
9. mu-calculus and proofs of communicating systems and
protocols.
Local model-checking.
Prerequisiti: Fondamenti di
Informatica
1. Fondamenti di Informatica 2.
Algoritmi e Strutture di Dati. Programmazione a oggetti e concorrente.
Modalità di esame:
Presentazione di un programma per la definizione della semantica
operazionale oppure per la verifica di correttezza di protocolli. Prova
scritta e orale.
Testi consigliati.
[Pe1] Pettorossi, A.: Quaderni di Informatica. Parte I - III,
UniTor (1991), Aracne (1993).
[PL] Pettorossi, A., Proietti, M.: First Order Predicate
Calculus
and Logic Programming, Aracne, 2002.
[Wi] Winskel, G.: The Formal Semantics of Programming
Languages:
An Introduction,
The MIT Press, 1993. (also available in Italian)
Errata
Corrige
-------------------------------------------------------------
This page should be stored in: pettorossi1:/home/adp/www/ProgramCorsoIT02-03.html