Obiettivi di apprendimento
L'obiettivo del corso è introdurre gli elementi di base della logica matematica e il suo uso per analizzare la correttezza di semplici programmi. Gli studenti impareranno a conoscere il calcolo proposizionale e la logica del primo ordine, e il loro utilizzo nella formalizzazione di enunciati dichiarativi in linguaggio naturale. Inoltre saranno in grado di utilizzare alcune tecniche formali di dimostrazione e di applicarle alla verifica di semplici programmi imperativi attraverso le triple di Hoare.
La prova scritta ha l'obiettivo di accertare che lo studente abbia acquisito sufficiente familiarita'nella dimostrazione di validita' di formule, nella formalizzazione di enunciati e nella verifica di triple di Hoare. Con la prova orale si verifichera' che lo studente abbia assimilato in modo critico i concetti introdotti nel corso.
Al termine del corso lo studente avra' consapevolezza dell'importanza di descrivere formalmente le proprieta' desiderate dei programmi e piu' in generale dell'importanza delle logiche per l'informatica. Sara' inoltre in grado di individuare e gestire casi di ambiguita' nella specifica di un programma.
L'accertamento delle capacita' avviene tramite colloquio nell'esame finale del corso.
Indicazioni metodologiche
- La frequenza e' fortemente consigliata.
- Le lezioni frontali si svolgono con uso di slide e della lavagna.
- Le esercitazioni si svolgono in aula: gli studenti svolgono degli esercizi, anche in gruppo, sotto la supervisione del docente.
- L'interazione con il docente avviene con colloqui (in orario di ricevimento o su appuntamento) e tramite posta elettronica.
- Sulla pagina web del corso vengono pubblicati progressivamente i lucidi presentati in ogni lezione, con riferimenti ai corrispondenti argomenti nei libri di testo. Vengono anche pubblicati i testi degli esercizi proposti per le esercitazioni.
- Il materiale didattico e alcuni esempi di testi di esame sono accessibile sulla pagina web del corso.
- Il corso prevede due prove intermedie il cui superamento esonera lo studente dalla prova scritta di esame.
Programma (contenuti dell'insegnamento)
- Introduzione alla logica matematica e sua rilevanza per la programmazione
- Calcolo proposizionale e tecniche di dimostrazione
- Calcolo dei predicati del primo ordine
- Formalizzazione di asserzioni in linguaggio naturale
- Intervalli di numeri e relativi connettivi
- Triple di Hoare per un sottoinsieme del linguaggio C
Bibliografia e materiale didattico
Slides presentate durante le lezioni e dispense scaricabili dalla pagina web del corso
Indicazioni per non frequentanti
Gli studenti non frequentanti possono trovare sulla pagina web del corso l'elenco degli argomenti presentati per ogni singola lezione, con le slide proiettate e i riferimenti al materiale didattico rilevante. Le modalita' d'esame per gli studenti non frequentanti sono identiche a quelle per gli studenti frequentanti.
Modalità d'esame
L'esame è composto da una prova scritta ed una prova orale. Il superamento di due prove in itinere equivale al superamento della prova scritta.
La prova scritta consiste in piú problemi da risolvere in circa due ore. Se superata, la prova rimane valida per tutti gli appelli della sessione di esami in corso.
La prova orale consiste in un colloquio tra il candidato e il docente, della durata di circa venti minuti.
- Teacher: FILIPPO BONCHI
- Teacher: ANDREA CORRADINI