Fondamenti - LINGUAGGI (2017/2018)

Codice insegnamento
4S02789
Docente
Massimo Merro
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
I sem. dal 2-ott-2017 al 31-gen-2018.

Per visualizzare la struttura dell'insegnamento a cui questo modulo appartiene, consultare * organizzazione dell'insegnamento

Orario lezioni

Vai all'orario delle lezioni

Obiettivi formativi

L’insegnamento si propone di fornire le basi teoriche dei linguaggi di programmazione appartenenti a tre diversi paradigmi di programmazione: imperativo, funzionale e concorrente. In particolare, vengono impartite tecniche per la definizione di semantiche formali e strumenti per l'analisi dei programmi a tempo di compilazione.

Al termine del corso lo studente sarà in grado di definire formalmente un nuovo linguaggio di programmazione, anche in un contesto di ricerca, attraverso una semantica operazionale formale e sistemi di tipi per l'analisi a tempo di compilazione della correttezza dei programmi scritti nel linguaggio.

Queste conoscenze consentiranno allo studente di: i) provare formalmente proprietà di correttezza di un'arbitraria semantica usando tecniche diverse di induzione; ii) provare formalmente la correttezza di un sistema di tipi; iii) padroneggiare equivalenze comportamentali semantiche per confrontare il comportamento dinamico di due programmi diversi.

Al termine del corso lo studente sarà in grado di: i) confrontare linguaggi diversi e scegliere tra questi il più adeguato a seconda del contesto d'uso e di fare le scelte progettuali più appropriate in fase di definizione di un nuovo linguaggio; ii) proseguire gli studi nell’ambito dei linguaggi di programmazione e dello sviluppo di software in maniera autonoma.

Programma

Lezioni frontali ed Esercitazioni (56 ore)

• Introduzione. Sistemi di transizione. La nozione di semantica operazionale strutturale. Sistema di transizioni per fornire la semantica operazionale di un semplice linguaggio imperativo. Opzioni per la progettazione di un linguaggio. Esercizi.

• Tipi. Introduzione ad un sistema formale di tipaggio. Tipaggio per un semplice linguaggio imperativo. Proprieta' di buon comportamento di programmi ben tipati. Esercizi.

• Induzione. Rivisitazione dell'induzione matematica. Alberi di sintassi astratta e induzione strutturale. Definizioni induttive guidate da un sistema di inferenze e "rule induction". Prove di proprieta' di safety. Esercizi.

• Linguaggi funzionali. Estensione del linguaggio base per la rappresentazione di funzioni higher-order. Tipaggio dell'estensione funzionale e semantica operazionale in modalita' call-by-value e call-by-name. Esercizi.

• Data. Semantica e tipaggio per strutture dati di tipo prodotto, somma, records, riferimenti. Esercizi.

• Sottotipaggio. Sottotipaggio dei record, funzioni, e codifica di un semplice linguaggio ad oggetti. Esercizi.

• Equivalenze semantiche. Equivalenze semantiche per frammenti di un semplice linguaggio imperativo. La proprieta' di congruenza di un'equivalenza semantica. Esempi di frammenti di programma equivalenti e non. Esercizi.

• Concorrenza. Interleaving con variabili condivise. Semantica per semplici mutex. Una proprieta' di serializzazione. Equivalenze semantiche in linguaggi concorrenti. Esercizi.

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Carl A. Gunter Semantics of Programming Languages MIT Press 1992 0262570955
Peter Sewell Semantics of Programming Languages (Edizione 5) Cambridge University Press 2017 Available at the web page of Peter Sewell.
G. Winskel The formal Semantics of Programming Languages MIT Press 1993

Modalità d'esame

Per superare l'esame lo studente dovrà dimostrare di essere in grado di:
* definire, attraverso regole di inferenza, semantiche operazionali e sistemi di tipo per semplici linguaggi imperativi, funzionali e concorrenti;
* provare formalmente proprietà su un'arbitraria semantica operazionale usando tecniche diverse di induzione (matematica, strutturale, rule-based);
* conoscere e usare diverse nozioni di equivalenze semantica per confrontare il comportamento di programmi scritti in linguaggi imperativi, funzionali e concorrenti.

L'esame consiste in una prova scritta composta da 4 o 5 esercizi. Lo svolgimento corretto di tutti gli esercizi consente di conseguire una votazione di 30/30.

Opinione studenti frequentanti - 2017/2018