Docente: Alberto
Pettorossi. You can talk to the teacher after the lectures or by
appointment.
Lectures: from 03.10.05 to 26.11.05
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:
14.09.06
10:30 (Room 6 n.e.)
Seminario
didattico-scientifico in preparazione all'esame
19.09.06
09:30 (Room 6 n.e.) Primo appello (*)
26.09.06 15:30 (Room 2 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, 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.
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 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.
[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
-------------------------------------------------------------