Corso di laurea in Informatica

Sono richieste conoscenze elementari di logica e buone conoscenze di programmazione e algoritmi; inoltre si assume che lo studente possegga nozioni di linguaggi formali.
Insegnamenti propedeutici (forniscono le competenze attese in ingresso): Matematica Discreta e Logica, Programmazione 1 e 2, Algoritmi e Strutture Dati, Linguaggi Formali e Traduttori.

L'insegnamento si propone di offrire agli studenti le conoscenze di base relative alla verifica formale di proprietà dei programmi. Gli obiettivi dell'insegnamento dei metodi formali fanno parte degli Obiettivi formativi specifici del CdS in Informatica (L31), in particolare sono tra quelli relativi all'area di approfondimento dell'informatica. A questo scopo vengono introdotte le basi teoriche dei sistemi di riscrittura, del lambda calcolo e della teoria dei tipi. Quindi sarà trattato un semplice linguaggio imperativo, di cui verranno esposti la semantica operazionale e quella logica, basata sulla logica di Hoare.

CONOSCENZA E CAPACITÀ DI COMPRENSIONE Acquisizione della conoscenza di alcune tecniche per la verifica formale della correttezza funzionale di programmi basate sulla logica e sulla specifica mediante "contratti".

CAPACITÀ DI APPLICARE CONOSCENZA E COMPRENSIONE Acquisizione della capacità di costruire dimostrazioni formali di correttezza dei programmi mediante l'uso di un tool, ed in particolare di proof-assistant.

AUTONOMIA DI GIUDIZIO Acquisizione di consapevole autonomia di giudizio con riferimento alla valutazione alla necessità di sviluppare il codice dei programmi in modo ben strutturato e di documentarlo in modo formalmente preciso per facilitarne la verifica ed assicurarne l'affidabilità.

ABILITÀ COMUNICATIVE Acquisizione di competenze e strumenti per la comunicazione nella forma scritta e orale per documentare la correttezza ed affidabilità dei programmi o al contrario per evidenziarne i punti deboli.

CAPACITÀ DI APPRENDIMENTO Acquisizione di capacità autonome di apprendimento e di autovalutazione della propria preparazione, atte ad intraprendere gli studi successivi con un alto grado di autonomia.

 

• Metodi formali
  • Logica equazionale e riscrittura
  • Deduzione naturale
  • Lambda calcolo
• Il sistema Agda
  • Funzioni e tipi di dato
  • Logica costruttiva
  • Liste e strutture dati
  • Verifica di programmi funzionali
• Fondamenti di linguaggi di programmazione procedurali
  • Sintassi del linguaggio IMP
  • Semantica operazionale big-step e small-step
  • Sistemi di tipo per IMP
  • Logica di Hoare
  • Completezza relativa
  • Verification conditions
  • Separation logic

Le lezioni si svolgeranno in presenza e verranno registrate. Le registrazioni, il testo, i lucidi, le dispense ed altro materiale didattico saranno forniti attraverso la pagina Moodle dell'insegnamento: https://informatica.i-learn.unito.it/course/view.php?id=2492

L'esame consiste in un colloquio orale in cui, oltre agli argomenti della teoria indicati nel programma, verranno verificate le competenze nell'uso dei tool adottati mediante l'esecuzione di brevi esercizi. Si terrà conto di eventuali prove in itinere ovvero di consegne la cui discussione sostituisce gli esercizi con i tool.