DISI Dipartimento di Informatica e Scienze dell'Informazione


Metodi Formali dell'Informatica

Oltre agli studenti nel cui piano di studi compare MFI, la seconda parte di MFI, ovvero quella riguardante le specifiche, deve essere sostenuta anche dagli studenti nel cui piano di studi compaiono MTI o ASD del 4 anno.
Questi ultimi sono invitati a contattare via email Maura Cerioli per verificare le modalità d'esame.

Programma schematico

Modalità degli Esami

Durante l'anno sono previste sei prove intermedie (5 durante il periodo delle lezioni ed una all'inizio del periodo di sospensione).
Chi ne abbia sostenuto almeno cinque, con media complessiva sufficiente, può presentarsi all'orale con tale media come voto di scritto.
Chi li abbia sostenuti tutti, con media complessiva sufficiente, può farsi registrare il voto corrispondente alla media.
I voti dei compitini sono validi fino all'appello di febbraio 2003 incluso.
Fallire un orale non annulla i compitini (ovvero sarà nuovamente possibile usarli come scritto negli appelli successivi).

Supervalutazione dei compitini

Come offerta di fine stagione, tenendo conto dello sforzo di prepararsi per 6 (diconsi 6) compitini e del fatto che la correzione dello scritto è inevitabilmente più rigorosa della valutazione durante un orale, è possibile farsi registrare come voto finale, senza sostenere l'orale, la media dei cinque migliori compitini o la media di tutti e sei i compitini incrementata del 10% (quale delle due risulti migliore).
Le medie calcolate si trovano qui (vi pregherei di verificare eventuali errori e comunicarmeli asap)

Attenzione: questa possibilità decade se si consegna uno scritto o sostiene un orale (ferma restando la regola generale di usare la media di 5 compitini, se sufficiente, come voto di scritto).

Appelli "standard"

Durante i periodi di sospensione saranno fissati appelli come d'uso.
Per sostenere l'esame in un appello è necessario prenotarsi via email.
Se non si verificano imprevisti di imponente entità non saranno concessi appelli straordinari.

Ogni scritto è valido esclusivamente nell'appello corrispondente (cioè bisogna sostenere l'orale nello stesso appello dello scritto) e consegnando uno scritto si cancella, limitatamente a quell'appello, un eventuale voto di compitini (che tornerà a valere a partire dall'appello successivo).

Fogli Esercizi etc

Registro delle lezioni

Per visualizzare correttamente il formato ps, si consiglia di impostare la visualizzazione su foglio A4.

Le lezioni con background di
questo colore
sono state/saranno tenute dalla Prof. Elena Zucca sul soggetto delle logiche assertive per linguaggi imperativi.

Il materiale relativo si trova qui

Novembre

Data Ora Aula Soggetto Materiale
5/11/2001 11-13 710 Introduzione ps, ppt
Semantica statica: concetti base ps, ppt
6/11/2001 11-13 710 Semantica statica delle espressioni tipate e non
7/11/2001 15-17 710 Semantica statica: ambienti locali, uso e gestione
Semantica statica: esercizi alla lavagna
8/11/2001 11-13 710 Semantica statica di LW: esercitazione guidata ps e ppt
9/11/2001 11-13 710 Semantica statica di LW: esercitazione guidata, continuazione
12/11/2001 11-13 710 Semantica Dinamica: concetti base ps e ppt
Semantica Denotazionale di Linguaggi imperativi
la nozione di ambiente
ps e ppt
13/11/2001 11-13 710 Semantica Denotazionale di Linguaggi imperativi
la nozione di stato
Semantica delle espressioni di LW
14/11/2001 15-17 710 Semantica delle dichiarazioni di LW
15/11/2001 11-13 710 Semantica degli statements di LW
Esercizi semantica statica
16/11/2001 9-11 710 Esercizi su semantica di funzioni ricorsive
19/11/2001 11-13 509 Prima prova Intermedia Questionario.ps e Esercizi.ps
Risultati
20/11/2001 11-13 710 Correzione della prima prova Intermedia
21/11/2001 15-17 710 Esercizi
22/11/2001 11-13 710 Esercizi
23/11/2001 9-11 710 Esercizi
26/11/2001 11-13 710 Semantica Operazionale Strutturata a grandi passi ps e ppt
27/11/2001 11-13 710 Semantica Operazionale Strutturata a piccoli passi
Espressioni e dichiarazioni
ps e ppt
28/11/2001 15-17 710 Semantica Operazionale Strutturata a piccoli passi
chiamata e dichiarazione di funzioni
29/11/2001 11-13 710 generalità su metodi di specifica;
introduzione informale delle asserzioni alla Hoare;
nozione di weakest precondition di un comando rispetto ad una postcondizione (correttezza totale);
weakest precondition per skip, concatenazione e if-then-else
ps e pdf
30/11/2001 9-11 710 Esercizi preparatori alla seconda prova

Dicembre

3/12/2001 11-13 509 Seconda prova Intermedia Questionario 2, pg1 e pg2
Compitino 2
Risultati
4/12/2001 11-13 710 Soluzione della seconda prova Questionario 2 pg1 e pg2
5/12/2001 15-17 710 Conclusione della correzione
SOS a piccoli passi: conclusione e lazy valuation
6/12/2001 11-13 710 EZ
7/12/2001 9-11 710 Esercizi
10/12/2001 11-13 710 Esercizi (conversione da decimale a binario in stile SOS-SS)
11/12/2001 11-13 710 Il frammento applicativo: semantica statica, denotazionale e operazionale a piccoli passi ps e ppt
12/12/2001 15-17 710 EZ
13/12/2001 11-13 710 SOS a piccoli passi per LF: conclusione
lambda-calcolo: beta-regola
ps e ppt
14/12/2001 9-11 710 lambda-calcolo: alfa-regola ed esercizi
17/12/2001 11-13 509 Terza prova Intermedia Questionario 3
Compitino 3
Risultati questionario
Risultati seconda parte
18/12/2001 11-13 710 Soluzione della terza prova Questionario 3
19/12/2001 15-17 710 EZ
20/12/2001 11-13 710 Soluzione della terza prova
Esercizi sul lambda-calcolo
21/12/2001 9-11 710 Esercizi sul lambda-calcolo

Gennaio

7/1/2002 11-13 710 Introduzione alla concorrenza
Modello a memoria condivisa
Il linguaggio ParWhile
Introduzione ps e ppt
Parwhile ps e ppt
8/1/2002 11-13 710 Esercizi sul ParWhile
9/1/2002 15-17 710 EZ
10/1/2002 11-13 710 Sistemi di transizione etichettati e CCS ppt e ps
11/1/2002 9-11 710 Semantica a tracce
Alberi di sincronizzazione
14/1/2002 11-13 710 Bisimulazione Forte
15/1/2002 11-13 710 Esercizi sulla bisimulazione forte e il ParWhile
16/1/2002 15-17 509 Quarta prova Intermedia Questionario 4
Compitino 4
Risultati questionario
Risultati seconda parte
Risultati Senza dettagli
17/1/2002 11-13 710 EZ
18/1/2002 9-11 710 Soluzione Quarta Prova Intermedia Questionario 4
21/1/2002 11-13 710 Specifiche algebriche
Algebre parziali con predicati
formule del prim'ordine parziali e validità
ppt, pdfe ps
22/1/2002 11-13 710 Uguaglianza, strettezza e definitezza.
Specifiche e validazione.
23/1/2002 15-17 710 EZ
24/1/2002 11-13 710 Esercizi su specifiche algebriche (interi)
25/1/2002 9-11 710 Modello iniziale e sistema di Birkhoff

Prove nel periodo di interruzione

30/1/2002 15-17 509 Quinta prova Intermedia Questionario 5
Soluzione questionario 5
Compitino 5
Risultati Senza dettagli
Risultati questionario
Risultati seconda parte
6/2/2002 Sesta prova Intermedia
20/2/2002 9-13 216 Scritto

Please send suggestions and comments to: Last Updated
Maura Cerioli cerioli@disi.unige.it
19 February, 2002