Descrizione del Corso

Programma del Corso

• Il Linguaggio LF
• Introduzione
• Tipi di dato naturali e booleani
• Sintassi del linguaggio LF
• Il vocabolario di LF
• Espressioni
• Definizione induttiva delle espressioni di LF
• Definizione delle espressioni di LF tramite una grammatica generativa
• Semantica operazionale naif di LF
• Uso della ricorsione ben fondata per definire funzioni
• Prove di proprieta` di programmi
• Terminazione
• Correttezza
• Il tipo stringa
• Tipi di dato ricorsivi: liste
• Specifica sintattica
• Specifica semantica
• Esempi di programmi su liste
• Tipi di dato ricorsivi: alberi binari
• Specifica sintattica
• Specifica semantica
• Esempi di programmi su alberi binari
• Visita di un albero
• Alberi di ricerca
• Il tipo prodotto cartesiano
• Semantica operazionale strutturata di LF
• Semantica a piccoli e a grandi passi
• Valutazione delle chiamate di funzione
• Dichiarazioni e blocchi
• Tipi
• Uso degli identificatori di costanti
• Dichiarazioni di costanti
• Il costrutto ``let''
• Semantica
• Regole di scoping
• Dichiarazioni di funzioni
• Semantica
• Chiamata di funzione
• Dichiarazione di funzione
• Significato computazionale di una dichiarazione di funzione
• Regole di scoping per le funzioni e i loro parametri
• Definizioni induttive di funzioni
• Principio di induzione associato ai sistemi induttivi
• Dominio di definizione di una funzione definita induttivamente
• Prove di proprieta`
• Semantica denotazionale di LF
• Funzioni di interpretazione semantica
• Corrispondenza fra la semantica denotazionale e la semantica operazionale strutturata
• Dichiarazioni e chiamate di funzioni
• Valutazione di espressioni con la semantica denotazionale
• Semantica statica
 
• Complementi: Teoria dell'Induzione
• Sistemi chiusi e generati rispetto ad un sistema di inferenza
• Appartenenza di stringhe a linguaggi definiti induttivamente
• Prove di proprieta' su insiemi definiti induttivamente
• Alberi di prova e problemi di ambiguita' di linguaggi
 
• Il linguaggio while
• Nozione di stato esterno ed interno.
• Variabili
• Input-output
• Il concetto di comando
• Istruzioni di assegnamento
• Istruzioni di input-output
• Comandi condizionali
• Comandi iterativi
• Il comando while
• Il comando repeat
• Il comando for
• Semantica statica e dinamica
• Il tipo array
• Il tipo record
• Annotazioni.
• Nozione semiformale di asserzione
• Nozione semiformale di invariante
• Concetto di correttezza
• Terminazione
• Esempi
• Il tipo puntatore
• Variabili statiche e dinamiche
• Semantica
• Implementazione di strutture dati dinamiche tramite puntatori
• Problemi di sharing
• Garbage collection
• Procedure e funzioni con comandi
• Dichiarazione
• Chiamata
• Parametri per valore e per riferimento
• Semantica
 
• Programmazione modulare
• Tipi di dato astratti
• Motivazioni
• Il concetto di tipo di dato come algebra eterogenea
• Specifica astratta
• Implementazione
• Implementazione di tipi di dato in linguaggi imperativi
• Operazioni che modificano lo stato
• Specifiche con asserzioni
• Specifiche concrete
• Liste con puntatori
• Liste con tipo "node"
• Liste bidirezionali
• Liste circolari
• Pile
• Code
• Realizzazione tramite liste
• Realizzazione tramite array
• Alberi con puntatori
• Alberi binari con tipo "node"
• Alberi n-ary
• Alberi generici
• Visita di un albero per livelli
• Grafi
• Realizzazione tramite puntatori
• Realizzazione tramite matrice delle adiacenze
• Visita di un grafo
 

Materiale didattico

• Per la parte di teoria: Dispense prodotte dai docenti.
• Per la parte di Pascal (laboratorio) "Introduzione al Pascal", di Jim Welsh e John Elder, pubblicato dalla ESA (Edizioni Scientifiche Associate).