elenco     
        corso     

Logica per la programmazione A

Codice: 009AACrediti: 6Semestre: 1Sigla: LpP 
 
Settore disciplinare: INF/01 - Informatica

Docente

Fabio Gadducci   gadducci@di.unipi.it  Home Page di Fabio Gadducci  Stanza 380  Tel. 0502212716

Ultima versione disponibile: programma da confermare per l’a.a. 2013/2014

Prerequisiti

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
Ore lezione: 60    

Bibliografia

Dispense scaricabli dalla pagina del corso:

Modalità di esame

Scritto (eventualmente sostituito dalle due prove intermedie)
e orale

Ulteriore pagina web del corso: http://www.di.unipi.it/~andrea/Didattica/LPP-12/


home


email