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.

CURRICULUM TIPO:

1° Anno 

2° Anno   Attivato nell'A.A. 2022/2023

InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Attivato nell'A.A. 2022/2023
InsegnamentiCreditiTAFSSD
Prova finale
24
E
-
Insegnamenti Crediti TAF SSD
Tra gli anni: 1°- 2°
Tra gli anni: 1°- 2°
Altre attività
3
F
-
Tra gli anni: 1°- 2°

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.




S Stage e tirocini presso imprese, enti pubblici o privati, ordini professionali

Codice insegnamento

4S008895

Crediti

12

Coordinatore

Massimo Merro

Lingua di erogazione

Italiano

Settore Scientifico Disciplinare (SSD)

ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI

L'insegnamento è organizzato come segue:

Teoria

Crediti

10

Periodo

Primo semestre

Laboratorio

Crediti

2

Periodo

Primo semestre

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

Visualizza la bibliografia con Leganto, strumento che il Sistema Bibliotecario mette a disposizione per recuperare i testi in programma d'esame in modo semplice e innovativo.

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.

Le/gli studentesse/studenti con disabilità o disturbi specifici di apprendimento (DSA), che intendano richiedere l'adattamento della prova d'esame, devono seguire le indicazioni riportate QUI