- Sintassi e semantica della logica del I ordine. Sintassi e
semantica operazionale dei linguaggi di programmazione
flowchart e while.
(scarica lucidi in formato pdf)
- Principio di induzione per i numeri naturali. Definizione
induttiva di insiemi. Esempi di insiemi definiti
induttivamente. Definizione costruttiva di insiemi definiti
induttivamente. Principio di induzione strutturale. Definizione
di funzioni per induzione.
(scarica
lucidi in formato pdf)
- Sintassi di un linguaggio di programmazione ricorsivo.
Interpretazione dei termini: valori indefiniti, ordini parziali
piatti, funzioni monotone. Semantica operazionale:
semplificazione, sostituzione, computazioni.
(scarica
lucidi in formato pdf)
- Ordini parziali completi e loro proprietà. Esempi. Funzioni
monotone e continue e loro proprietà. Esempio sui programmi
ricorsivi. Teorema del punto fisso ed esempio di applicazione.
Semantica denotazionale dei programmi ricorsivi: sintassi e
semantica della lambda-notazione, definizione del funzionale
semantico, definizione di semantica denotazionale.
(scarica
lucidi in formato pdf)
- Semantica denotazionale dei programmi while. equivalenza
semantica operazionale e denotazionale per il programmi while.
Esempio. Verifica dei programmi: specifiche di correttezza
(parziale e totale) e di terminazione. Precondizioni più
deboli e postcondizioni più forti per programmi flowchart e
while. Esempi di verifica di correttezza parziale e totale per
un programma flowchart.
(scarica
lucidi in formato pdf)
- Esempi di dimostrazione di terminazione e correttezza
totale per due programmi ricorsivi. Il metodo delle asserzioni
induttive per la dimostrazione di parziale correttezza dei
programmi flowchart: cammini, correttezza parziale di programmi
e cammini, dimostrazione di correttezza del metodo.
(scarica
lucidi in formato pdf)
|