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'obiettivo del modulo è quello di presentare le basi teoriche dei linguaggi di programmazione. A tale scopo verranno introdotti vari linguaggi paradigmatici, anche di ordine superiore. Il modulo sarà incentrato sui concetti di semantica operazionale e di sistema di tipo. Verranno introdotte alcune tecniche formali per la verifica del comportamento dei programmi.

Al termine del modulo 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 frammenti di programmi scritti in linguaggi imperativi, funzionali e concorrenti.

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 2016
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.