Fondamenti di linguaggi di programmazione e specifica (2020/2021)



Codice insegnamento
4S008895
Crediti
12
Coordinatore
Massimo Merro
Settore disciplinare
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Lingua di erogazione
Italiano
L'insegnamento è organizzato come segue:
Attività Crediti Periodo Docenti Orario
Teoria 10 I semestre Maria Paola Bonacina, Massimo Merro

Vai all'orario delle lezioni

Laboratorio 2 I semestre Massimo Merro

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 affrontate le seguenti tematiche: (i) tecniche per la definizione di sintassi e semantiche formali, (ii) logiche per esprimere proprietà formali di buon comportamento di programmi, (iii) strumenti per l'analisi statica dei programmi, (iv) nozioni di equivalenze comportamentali tra programmi. Al termine del corso, lo studente sarà in grado di definire formalmente un nuovo linguaggio di programmazione, anche in un contesto di ricerca, attraverso sintassi, semantica formale e sistemi di tipi per l’analisi statica della correttezza dei programmi scritti nel linguaggio. Sarà inoltre in grado di esprimere attraverso linguaggi logici proprietà di buon comportamento dei programmi. Queste conoscenze consentiranno allo studente di: i) provare formalmente proprietà di correttezza di un'arbitraria semantica usando tecniche diverse di induzione; ii) provare formalmente se un programma soddisfa una determinata proprietà di buon comportamento; iii) provare formalmente la correttezza di un sistema di tipi; iv) padroneggiare equivalenze comportamentali semantiche al fine di confrontare il comportamento, a tempo di esecuzione, 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

Prima parte.

• 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. Proprietà 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 proprietà di safety. Esercizi.

• Linguaggi funzionali. Estensione del linguaggio base per la rappresentazione di funzioni higher-order. Tipaggio dell'estensione funzionale e semantica operazionale in modalità 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 proprietà 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 proprietà di serializzazione. Equivalenze semantiche in linguaggi concorrenti. Esercizi.

Seconda parte.

• Relazioni di ordinamento, reticoli, teoremi del punto fisso. Esercizi.

• Semantica denotazione di un linguaggio di programmazione imperativo. Esercizi.

• Esempi di proprietà di programmi e linguaggi di specifica. Esercizi.

• Logica di Hoare (completezza e incompletezza); correttezza parziale/totale. Esercizi.

• Decidibilità, safety, liveness, e sicurezza. Esercizi.

• Semantica a tracce - strutture di Kripke. Esercizi.

• Elementi di logiche temporali. 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 3 esercizi. Lo svolgimento corretto di tutti gli esercizi consente di conseguire una votazione di 30/30.

Testi di riferimento
Attività Autore Titolo Casa editrice Anno ISBN Note
Teoria Dovier A. Giacobazzi R. Fondamenti dell'Informatica: Linguaggi Formali, Calcolabilità e Complessità. Bollati Boringhieri 2020 9788833933795
Teoria Peter Sewell Semantics of Programming Languages (Edizione 6) Cambridge University Press 2019
Teoria Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741
Teoria G. Winskel The formal Semantics of Programming Languages MIT Press 1993