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.6. Verifica di protocolli e programmi concorrenti: il nu-calculo modale.
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.
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.
This page should be stored in: pettorossi1:/home/adp/www/ProgramCorsoIT00-01.html