Codice insegnamento

4S02789

Docente

Massimo Merro

Crediti

6

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

INF/01 - INFORMATICA

Periodo

I semestre dal 1 ott 2018 al 31 gen 2019.

Pagina Web

http://profs.scienze.univr.it/~merro/linguaggi.html

Orario Lezioni Moodle Seminari 0

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

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.

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.