Docente: Alberto
Pettorossi. You can talk to the teacher after the lectures or by
appointment.
Lectures: from 29.09.03 to 21.11.03
Monday 16:00-17:45 (Room 10 n.e.)
Tuesday 11:30-13:15 (Room 09 n.e.)
Friday 11:30-11:15 (Room 10 n.e.)
Exams: Wednesday
26.11.03
15:00 (Room 11 n.e.)
Wednesday 03.12.03 15:00 (Room 11 n.e.)
14.09.04 10:00 (Room 6 n.e.)
Seminario didattico scientifico su argomenti di esame
16.09.04 10:00 (Room 6 n.e.)
Primo Appello (*)
28.09.04 14:30 (Room 6 n.e.) Secondo Appello (*)
---
(*) 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 a oggetti e concorrente.
Modalità di esame:
(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.
Esercizi e progetti debbono essere svolti 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
-------------------------------------------------------------
This page should be stored in: pettorossi1:/home/adp/www/ProgramCorsoIT03-04.html