Dipartimento di Informatica, Sistemi e Produzione.  Computer Science Department.
Università di Roma Tor Vergata.

Docente: Alberto Pettorossi.
Wednesday 11:30-13:15 (Room 10)
Thursday     11:30-13:15 (Room 12)
Friday            9:30-11:15 (Room 12)
Lectures: from 10.12.01 to 15.2.02.
You can talk to Alberto Pettorossi 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.

Programma del corso:

1. Preliminary Notions and Program Correctness. [PE1 Chapter 1 and 8]
2. Funzioni Parziali Ricorsive.
3. Richiami di Calcolo dei Predicati e Programmazione Logica.
4. Teoria del Punto Fisso.
5. Semantica dei linguaggi di programmazione:

5.1 Semantica operazionale di linguaggi imperativi.
5.2 Semantica assiomatica di linguaggi imperativi. Calcolo delle triple di Hoare. Sua
        completezza.
5.3 Semantica dei linguaggi logici.
5.4 Introduzione alla teoria dei domini. Tecniche per la ricorsione.
       Teorema di Bekic e Teorema di ricorsione.
5.5 Semantica operazionale e denotazionale di  linguaggi funzionali del primo ordine:
        semantica by value e by name.
5.6 Semantica operazionale e denotazionale di linguaggi funzionali di ordine elevato:
        semantica by value e by name. Teoria dei tipi.
5.7 Nondeterminismo: guarded commands di Dijkstra.
5.8 Parallelismo e concorrenza: linguaggio CCS di Milner.

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 progetto per la definizione della semantica e/o
la verifica di correttezza di programmi logici o concorrenti facendo uso di strumenti quali il
Concurrency Workbench o il Map  per la trasformazione dei programmi oppure sviluppando un
programma  in Prolog.
Prova scritta e orale.

Testi consigliati.
[Pe1] Pettorossi, A.: Quaderni di Informatica. Parte I, UniTor (1991).
[Pe3] Pettorossi, A.: Quaderni di Informatica. Parte III, Aracne (1993).
[PL] Pettorossi, A.:  Predicate Calculus and Logic Programming, Aracne 2002
[Wi]  Winskel, G.: The Formal Semantics of Programming Languages: An Introduction,
                  The MIT Press, 1993. (available also in Italian)

Go to the top of the page.

This page should be stored in:  pettorossi1:/home/adp/www/ProgramCorsoIT01-02.html