Logica per la programmazione A

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

Docenti

Andrea Corradini   Questo indirizzo email è protetto dagli spambots. È necessario abilitare JavaScript per vederlo.   Home Page di Andrea Corradini  Stanza 357  Tel. 0502212786
Maria Simi   Questo indirizzo email è protetto dagli spambots. È necessario abilitare JavaScript per vederlo.   Home Page di Maria Simi  Stanza 365  Tel. 0502212758

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.

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: 38Ore esercitazione: 16  

Bibliografia

Dispense scaricabli dalla pagina del corso:

Modalità esame

Scritto (eventualmente sostituito dalle due prove intermedie)
e orale

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