- Oggetto:
- Oggetto:
Metodi Formali dell'Informatica - Parte A
- Oggetto:
Formal Methods in Computer Science - A
- Oggetto:
Anno accademico 2022/2023
- Codice dell'attività didattica
- INF0190
- Docente
- Ugo De' Liguoro (Corso A)
- Corso di studi
- [008707] Laurea in Informatica
- Anno
- 3° anno
- Periodo didattico
- Primo semestre
- Tipologia
- A scelta dello studente
- Crediti/Valenza
- 6 CFU - Numero di ore - Number of hours: 48 (in aula)
- SSD dell'attività didattica
- INF/01 - informatica
- Modalità di erogazione
- Tradizionale
- Lingua di insegnamento
- Italiano
- Modalità di frequenza
- Facoltativa
- Tipologia d'esame
- Orale
- Prerequisiti
-
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.The students is expected to have elementary knowledge of logic and good competencies in programming and algorithms, as well as some notions on formal languages.
Preparatory Courses (providing the expected entry skills): Matematica Discreta e Logica, Programmazione 1 e 2, Algoritmi e Strutture Dati, Linguaggi Formali e Traduttori. - Oggetto:
Sommario insegnamento
- Oggetto:
Obiettivi formativi
Il corso 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.The course aims to offer basic knowledge about some techniques of formal verification of programs. We introduce the theoretical foundations of term rewriting, lambda-calculus and type theory. Then we will consider a simple procedural programming language, its operational semantics and verification methods based on Hoare Logic. .- Oggetto:
Risultati dell'apprendimento attesi
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.
KNOWLEDGE AND UNDERSTANDING Acquisition of theoretical and applicative skills for the functional verification of programs, based on logic and on program specifications by means of "contracts".
APPLYING KNOWLEDGE AND UNDERSTANDING Acquisition of the ability to construct formal proofs of correctness of programs w.r.t. formal specifications by means of proof assistants.
MAKING JUDGEMENTS Acquisition of aware judgment autonomy concerning the need to design and code well-structured programs and document them precisely with the aim to make easier their verification and ensure their affordability.
COMMUNICATION SKILLS Acquisition of oral and written communication skills and expertise as well as the ability to document the correctness and affordability of programs, or to make evident their weaknesses.
LEARNING SKILLS Acquisition of autonomous learning capacity and self-assessment of its
preparation, in order to undertake subsequent studies with a high degree of autonomy.- Oggetto:
Modalità di insegnamento
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=2492Lectures will be in classes and they will be recorded. Recordings, texts, slides and handouts as well as code and other material will be available on the course page on the Moodle platform: https://informatica.i-learn.unito.it/course/view.php?id=2492- Oggetto:
Modalità di verifica dell'apprendimento
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.The exam will consist of an oral discussion where besides the topics of the theory as indicated in the syllabus, students' competence in the usage of the tools used in the classes and exercises will be checked by means of simple exercises. This last part can be replaced by ongoing tests and the discussion of assignments prepared using the tools.- Oggetto:
Programma
- Metodi formali
- Logica equazionale e riscrittura
- Deduzione naturale
- Lambda calcolo
- Il sistema Agda
- Funzioni e tipi di dato
- Logica costruttiva
- Fondamenti di linguaggi di programmazione procedurali
- Sintassi del linguaggio IMP
- Semantica operazionale big-step e small-step
- Logica di Hoare
- Completezza relativa
- Verification conditions
- Formal methods
- Equational reasoning and term rewriting
- Natural deduction
- Lambda calculus
- The Agda system
- Functions and data
- Constructive logic
- Foundation of procedural programming languages
- Syntax of the language IMP
- Big-step and small-step operational semantics
- Hoare logic
- Relative completeness
- Verification conditions
- Metodi formali
Testi consigliati e bibliografia
- Oggetto:
- Altro
- Titolo:
- Il testo principale del corso è: L. Padovani, U. de' Liguoro: Introduction to Program Verification. Il testo, consistente in pagine html, verrà fornito attraverso la piattaforma Moodle.
- Obbligatorio:
- No
- Oggetto:
Utili riferimenti sono i testi qui sotto citati, anche se utilizzano proof assistant differenti:
- Philip Wadler: Programming Language Foundations in Agda (PLFA)
- Tobias Nipkow, Gerwin Klein: Concrete semantics
- Adam Chlipala: Formal Reasoning About Programs
- Oggetto: