| | | corso | | | | | |
Logica per la programmazione A
Codice: | 009AA | Crediti: | 6 | Semestre: | 1 | Sigla: | LpP | |
|
Settore disciplinare: | INF/01 - Informatica |
Docente
Andrea Corradini
Tel. 0502212786Prerequisiti
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.
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