| | | corso | | | | | |
Logica per la programmazione B
Codice: | 009AA | Crediti: | 6 | Semestre: | 1 | Sigla: | LpP | |
|
Settore disciplinare: | INF/01 - Informatica |
Docente
Francesca Levi
Tel. 0502212770Prerequisiti
Nessuno
Obiettivi di apprendimento
Il corso si pone l'obiettivo di introdurre alcuni elementi basici della logica matematica e del suo utilizzo per analizzare la correttezza di semplici programmi.
Conoscenze.
Lo studente al termine del corso avrà acquisito familiarità con il Calcolo Proposizionale, con la Logica del Primo Ordine, con le Triple di Hoare, con alcune tecniche di dimostrazione e di verifica, e con la formalizzazione di asserzioni in linguaggio naturale.
Capacità.
Comportamenti.
Descrizione
Il corso introduce alcuni concetti elementari della Logica Matematica e del suo utilizzo per la verifica di semplici programmi. Dapprima viene introdotto il Calcolo Proposizionale, con varie tecniche di dimostrazione per verificare se una formula è una tautologia. Successivamente viene presentato il Calcolo dei Predicati del primo ordine (la sua sintassi, la semantica, e alcune leggi per i quantificatori) e ci si sofferma sulla formalizzazione nella logica proposta di asserzioni in linguaggio naturale. Quindi si presentano ulteriori quantificatori su sequenze di numeri naturali molto comuni in programmazione, e infine si presentano le triple di Hoare come strumento formale per la specifica e la verifica di semplici programmi imperativi.
Indicazioni metodologiche
Gli studenti sono invitati a organizzare il processo di apprendimento in moduli flessibili corrispondent ai vari argomenti presentati nel corso, posti in sequenza logica. Inoltre essi sono invitati a valutare in corso di erogazione il livello di raggiungimento degli obiettivi utilizzando
in modo critico le esercitazioni in aula e gli strumenti delle verifiche intermedie.
Programma
- Introduzione alla logica matematica e sua rilevanza in programmazione
- Il Calcolo Proposizionale
- Tecniche di dimostrazione
- Il Calcolo dei Predicati del primo ordine
- Formalizzazione di asserzioni in linguaggio naturale
- Connettivi su intervalli di numeri
- Le Triple di Hoare
Bibliografia
Dispense scaricabli dalla pagina del corso:
Modalità di esame
Scritto (eventualmente sostituito dalle due prove intermedie)
e orale