Docente: Alberto
Pettorossi.
You can talk to the teacher
after the lectures or by
appointment.
Lectures: from 02.10.06 to 24.11.06
Monday 16:00-17:45 (Room 10 n.e.)
Tuesday 09:30-11:15 (Room 08 n.e.)
Friday 11:30-13:15 (Room 10 n.e.)
Exams:
Thursday 30.11.06
15:00 (Room 12 n.e.)
(*)
Tuesday 05.12.06 15:00 (Room 12 n.e.)
(*)
Tuesday
18.09.07
16:30 (Room 09 n.e.)
Seminario
didattico-scientifico in preparazione all'esame
Thursday 20.09.07
10:00 (Room 06 n.e.) Primo
appello (*)
Tuesday
25.09.07 10:00
(Room 06 n.e.) Secondo appello (*)
---
(*)
Contattare personalmente il docente. Non
ci si puo` prenotare a entrambi gli appelli.
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 e concorrenti. 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.
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.
Algoritmi e Strutture di Dati.
Programmazione orientata agli oggetti oppure Programmazione a oggetti e
concorrente.
Modalità di esame (indicazioni
di
massima):
(i) Voto nell'intervallo 18 - 20: Presentazione di 5 esercizi a scelta
del take-home-exam + Progetto P1 + Orale.
(ii) Voto nell'intervallo 21 - 25: Presentazione di 10 esercizi a
scelta
del take-home-exam + Progetti P1 e P2 + Orale.
(iii) Voto nell'intervallo 26 - 30 e lode: Presentazione di 15 esercizi
a
scelta del take-home-exam + Progetti P1 e P2 e P3 + Orale.
Nota: gli esercizi e i progetti debbono essere fatti dallo studente da
solo.
Testi consigliati.
[P] Pettorossi, A.: Elements of Computability, Decidability, and
Complexity,
Aracne (2006).
[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
-------------------------------------------------------------