Studiare
In questa sezione è possibile reperire le informazioni riguardanti l'organizzazione pratica del corso, lo svolgimento delle attività didattiche, le opportunità formative e i contatti utili durante tutto il percorso di studi, fino al conseguimento del titolo finale.
Piano Didattico
Il piano didattico è l'elenco degli insegnamenti e delle altre attività formative che devono essere sostenute nel corso della propria carriera universitaria.
Selezionare il piano didattico in base all'anno accademico di iscrizione.
1° Anno
2° Anno Attivato nell'A.A. 2022/2023
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
Insegnamenti | Crediti | TAF | SSD |
---|
4 insegnamenti a scelta
2 insegnamenti a scelta (A.A. 2022/23 Quantum computing non erogato)
3 insegnamenti a scelta (A.A. 2022/23 Quantum computing non erogato)
Legenda | Tipo Attività Formativa (TAF)
TAF (Tipologia Attività Formativa) Tutti gli insegnamenti e le attività sono classificate in diversi tipi di attività formativa, indicati da una lettera.
Fondamenti di linguaggi di programmazione e specifica (2021/2022)
Codice insegnamento
4S008895
Crediti
12
Lingua di erogazione
Italiano
Settore Scientifico Disciplinare (SSD)
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
L'insegnamento è organizzato come segue:
Teoria
Laboratorio
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.
Bibliografia
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 esercizi. Lo svolgimento corretto di tutti gli esercizi consente di conseguire una votazione di 30/30.