Vi prego di segnalarmi qualsiasi errore o imprecisione a: Laurent.Thery@sophia.inria.fr
Soluzione degli esercizi I,II,III,IV,V.
Download queste note Windows, Unix, Pdf.
Download le versioni con la vecchia sintassa Windows, Unix, Pdf.
true: bool
1: nat
"hello": string
Il linguaggio di Coq è funzionale. Il simbolo -> è utilizzato per rappresentare il tipo delle funzioni.
Per esempio, una funzione f che prende un numero naturale e restituisce un booleano si rappresenta come
f: nat -> bool. La parte Definizioni presenta in modo più completo il linguaggio.
Questa parte spiega come si possono definire, nel mondo della programmazione, nuove costanti, nuove funzioni e, simmetricamente nel mondo della prova,
nuovi predicati, nuove relazioni.
La difficoltà di questa parte è principalmente quella di acquisire familiarità
con la nozione di programmazione tipata.
La seconda parte Costruzioni induttive si occupa di come definire nuove strutture dati e come manipolarle. Una struttura dati è definita tramite un elenco degli oggetti che la compongono, ed ogni elemento in questo elenco rappresenta un costruttore, ovvero un modo di costruire un oggetto. Questo è importante perche' permette di fare delle discussioni (analisi) con la costruzione match .. with .. end sulla natura di un oggetto. Per esempio, questo è il meccanismo di base che permette di far cambiare il comportamento di una definizione in funzione dei valori dei suoi argomenti. Molti esempi illustrano come questi meccanismi di definizioni induttive e di discussione possono essere utilizzati. Una prima difficoltà di questa parte è di nuovo quella di acquisire familiarità con questi nuovi meccanismi. Una seconda difficoltà consiste nel capire come questi meccanismi possono essere utilizzati nello stesso modo nel mondo della programmazione e nel mondo della prova.
Questa parte introduce nuovi concetti di programmazione con cui bisogna acquisire familiarità. Per esercitarsi, questa pagina contiene tutti i compiti precedenti. Per qualsiasi domanda o problema, si prega di contattare il docente.
Considerato il fatto che questa parte del corso non è stata insegnata quest'anno, si dà la possibilità di fare, alternativamente alla usuale prova di esame, un progettino. Gli studenti che sono interessati a consegnare tale progetto sono invitati a contattare con sufficiente anticipo il docente.