Università degli Studi di Milano
Corso di Studi in Informatica, A.A. 2005-2006

Ricevimento studenti:

• M. Ornaghi: Venerdì ore 11.30

Materiale didattico:

• Il materiale didattico verra' pubblicato in rete durante lo svolgimento del corso sotto forma di dispense

Breve introduzione al corso

Premessa: da quest'anno accademico Metodi Formali 2 non sarà più in cascata con Metodi Formali 1, ovvero non richiederà nozioni introdotte in Metodi Formali 1.

Il programma:

• Parte I. JML: Java Modeling Language. Verrà introdotto il linguaggio di specifica e verifica JML. Tale linguaggio consente di documentare programmi Java con delle specifiche eseguibili, ovvero testabili RUN time. Fornisce metodi di verifica mediante test empirico ed analisi statica. La I parte occuperà circa i 2/3 del corso.
• Parte II. COOML: Constructive OO Modeling Language. Il linguaggio COOML ha caratteristiche simili a JML e a OCL (Object Constraint Language), ma ha come base semantica una logica costruttiva. E' attualmente in fase di sviluppo presso il Dipartimento di Scienze dell'Informazione. Questa parte del corso è pensata in funzione di possibili tesi di laurea magistrale.

L'esame: 2 prove in itinere. La prima prova riguarderà la prima parte del corso e può prevedere, a scelta, lo sviluppo di un piccolo progetto. La seconda prova, orale, riguarderà la seconda parte del corso.

Calendario e prove in itinere

• Inizio: 6 marzo 2006, fine: maggio 2006
• Prima prova: fine aprile 2006, data da concordare
• Prova finale: giugno 2006, data da concordare

Nelle prime lezioni si concorderanno possibili modifiche d'orario, in base alle esigenze degli studenti e compatibilmente con la disponibilità di aule