Logica per la programmazione A

Nessuno

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.

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.

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.

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.  

Dispense scaricabli dalla pagina del corso:

• [LP1] Logica per la Programmazione
• [LP2] Logica per la Programmazione 2
• [LdH] Logica di Hoare

Scritto (eventualmente sostituito dalle due prove intermedie)
e orale