Corso di Informatica Teorica. Anno Accademico 2000-2001.

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

Docente: Alberto Pettorossi.

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.

On-line lecture notes:  click here first.

Programma del corso:

1. Correttezza dei programmi. [PE1 Chapter 8]
2. Funzioni Parziali Ricorsive. Lambda Calcolo.
3. 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 CSP di Hoare, linguaggio CCS di Milner.
6. Verifica di  protocolli e programmi concorrenti: il nu-calculo modale.

Prerequisiti: Fondamenti di Informatica 1, 2, 3 e 4.

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.
Prova orale.

Testi consigliati.
[Me] Mendelson, E.: Introduction to Mathematical Logic, Wadsworth & Brooks/Cole
                  Advanced Books & Software, Monterey, California. 1984.
[Pe1] Pettorossi, A.: Quaderni di Informatica. Parte I, UniTor (1991).
[Pe3] Pettorossi, A.: Quaderni di Informatica. Parte III, Aracne (1993).
                            Download here: Decidability Notes.
                            Download here: Partial Recursive Functions.
[PL] Pettorossi, A.: Notes on Predicate Calculus and Logic Programming, Lecture Notes, 1998.
[Wi]  Winskel, G.: The Formal Semantics of Programming Languages: An Introduction,
                  The MIT Press, 1993.

Go to the top of the page.

This page should be stored in:  pettorossi1:/home/adp/www/ProgramCorsoIT00-01.html