picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

[Diario 2004/05] Metodi Formali dell'informatica 1 e 2

Il corso è tenuto dal prof. Mario Ornaghi nel primo semestre in auletta 5 con il seguente orario:

lunedì 10.30-12.30
martedì 15.30-17.30
mercoledì 14.30-16.30

alle lezioni del modulo uno che termineranno approssimativamente a metà semestre seguiranno quelle del modulo due.

Per gli studenti della Quinquennale: l'esame è unico (modulo1+modulo2) 12 cfu
Per gli studenti della Specialistica: gli esami sono due complementari da 6 cfu ciascuno (si può fare anke solo il primo)
Per gli studenti della Triennale: l'unico esame nel manifesto di studi è il modulo 1 da 6 cfu, resta però da verificare se uno studente può fare un'esame della specialistica portandosi avanti (ne discuteranno i prof a breve!)

Modalità d'esame:
2 compitini per il modulo 1 o l'orale
2 compitini per il modulo 2 o l'orale
(per chi deve fare 12 cfu c'è un esame unico); non c'è data d'appello per l'orale ma va concordata col docente.

Materiale didattico per modulo 1:
Warmer-Kleppe: OCL
fotocopie dei lucidi e dispense
specifiche in rete
(Il materiale per il modulo 2 sarà comunicato in seguito).

Le dispense non saranno pubblicate ma saranno mandate direttamente tramite mail dal docente, gli studenti presenti oggi hanno già dato il loro indirizzo mail, chiunque voglia ricevere le dispense sia che frequenti le lezioni sia che non frequenti deve mandare una e-mail al professore.

Programmi:
Modulo 1

• Aspetti semiformali e formali della programmazione OO
  - UML (Unified Modeling Language)
  - OCL (Object Constraint Language)
  . semantica formale
  . tools e uso nel testing
  

Modulo 2

• Metodi formali per Java
  - JML (Java Modeling Language)
  - Tools per JML, per testing e verifica formale
  

Prerequisiti:
conoscenza di un linguaggio OO (tutti i presenti hanno detto di conoscere Java e quindi non sarà ripreso a lezione)
qualche conoscenza di logica sarebbe utile ma saranno comunque fatti richiami su queste nozioni.

La prima lezione di oggi è stata solo introduttiva al corso le lezioni vere e proprie inizieranno domani.

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Valutando le varie esigenze degli studenti abbiamo concordato di gestire i quarti d'ora accademici in questo modo:

lunedì 11:00-12:30
martedì 15:45-17:15
mercoledì 14:30-16:00


La lezione di oggi è la prima di una serie di 3 o 4 lezioni che riprendono e trattano UML e alcuni aspetti di Programmazione ad Oggetti.

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

In questa lezione sono stati fatti alcuni esempi di modellazione di realtà tramite l'uso di diagrammi di classe e diagrammi di oggetti UML.

Altri argomenti: semantica type->instance, semantica delle associazioni, informazioni sui diagrammi (nome, ruolo, molteplicità, aggregazione, navigazione, qualificazione).

Sulla falsa riga di questi tipi di esercizi verterà il primo dei due compitini previsti.

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Argomenti trattati:

I vincoli (elementi di sintassi e di semantica per segnature e navigazioni)
Espressioni sintassi e semantica informale
Invarianti e contratti

Lunedì saranno svolti diversi esercizi su questi argomenti

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

lunedì e martedì sono stati svolti vari esercizi, con mercoledì son concluse le spiegazioni per i seguenti argomenti:

Vincoli: invarianti e contratti
Dimostrazioni di invarianza
Teorema di invarianza

AVVISO:
Lunedì 18 e martedì 19 ci saranno 2 lezioni di richiami di logica.
Si proseguira' anche con gli esercizi di preparazione al primo compitino.
Mercoledì 20 lezione di preparazione al compitino, con domande
tipo ed esercizi.

La settimana successiva, in data da concordare, il primo compitino.

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

AVVISO il primo compitino si farà mercoledì 3 novembre in orario e luogo ancora da decidere.

Le lezioni di logica di lunedì 18 e martedì 19 comprendono i seguenti argomenti:

Generalità sui sistemi di rappresentazione della conoscenza e assunzioni “ontologiche” per sistemi basati sulla logica del primo ordine. La sintassi dei linguaggi del primo ordine e definizioni di epressioni, formule, overloading, termini ed atomiche ground, formule chiuse.
Semantica della logica del primo ordine e semantica di istanza UML. Interpretazioni di una segnatura
Interpretazione dei termini e delle formule.

Mercoledì è stato letto il programma dettagliato per il primo compitino e sono state date queste indicazioni:
Sulla parte di UML ci saranno principalmente esercizi anche se possono esserci qualche domanda di teoria, domande varie verteranno di più sulla parte dei vincoli e della logica.
Gli argomenti compresi nel primo compitino saranno quelli fatti fino al 19 ottobre, settimana prossima si proseguirà a fare esercizi in preparazione.

Il prigramma dettagliato è il seguente:

UML
• Generalità su UML. Elementi di sintassi: simboli grafici, cammini,
stringhe. Diagrammi e viste.
• I diagrammi di classe (sintassi grafica per classi, relazioni fra classi,
classi astratte, …) e i diagrammi di oggetti (sintassi grafica per
oggetti e link).
• Associazioni, diversi tipi di associazioni, molteplicità, ruoli.
• Semantica di istanza per classi, generalizzazione (classi come tipo
e implementative), associazioni (con annessi, come molteplicità),
diagrammi di classe.
VINCOLI.
• I vincoli: la nozione di vincolo come predicato.
• Semi-formalismo didattico per scrivere vincoli nel contesto di una
classe: principalmente a livello di esercizi. Usare correttamente e
nel modo dato sulla dispensa le navigazioni (con i loro tipi); per il
resto, si accettano variazioni, purché sensate.
• Invarianti: definizione di invariante, il principio di sostituzione e
covarianza.
• Contratti per query. Principio di sostituzione e contro-covarianza.
• Contratti per azioni. Definizione. Uso di @pre.
• Teorema di invarianza.
RICHIAMI di LOGICA
• Definizione di segnatura del primo ordine Σ = (T,Ω)
– assunzioni ontologiche
– overloading
• Definizione di EXPRt, Atomica e Formula in una segnatura.
– variabili libere e vincolate, formule chiuse ed aperte
• Definizione di interpretazione I di una segnatura
– legame con UML, a livello di esempi

Last edited by picoid82 on 22-10-2004 at 14:58

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Gli argomenti trattati in queste lezioni non faranno parte del primo compitino.

Questa settimana sono stati trattati:
- Teorie, Modelli, Completezza (lez.11)
- Introduzione ad OCL (lez.12e13)

Il primo compitino si svolgerà in aula delta ora 14:00 il giorno mercoledì 3 novembre

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

- lunedì 8 è stato corretto il primo compitino

- martedì 9 prima lezione su OCL con lettura dell'appendice delle specifiche 2.0

a tre lezioni di teoria seguiranno lezioni di laboratorio, per fine novembre è prevista la seconda prova di vaalutazione, che può essere una prova di laboratorio o un piccolo progetto (UML+OCL) da svolgere anche a gruppi

sempre a fine novembre inizieranno le lezioni per il secondo modulo che avrà altri due compitini e un voto separato

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Come forse già sapete il professore è infortunato, ha detto che comunicherà come proseguire il corso, se arriverà un sostituto o se il modulo 1 si concluderà con un progettino proposto da noi..
ulteriori comunicazioni saranno rese visibili anche qui..

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

La prossima lezione sarà lunedì 13 dicembre ore 11 auletta 5, sarà la prima di (credo) 3 lezioni di laboratorio.

La parte di teoria si è conclusa con la lettura dell'appendice A delle specifiche OCL (fino A.28.. sarò più preciso in seguito..)

Il secondo voto che darà luogo al voto finale del modulo 1 sarà sul progettino dell'agenda elettronica (avremo dettagli maggiori in seguito) che sarà valutato a gennaio.

A seguito inizieranno le lezioni del Modulo 2 che si protrarranno anche nel mese di febbraio..

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Iniziamo qui le discussioni in merito al progetto dato per avere la seconda valutazione per il primo modulo del corso.

Vi introduco le indicazione date dal professore che prenderà comunque parte al forum:

a) viene valutato principalmente il modello UML con i relativi vincoli OCL (Argo, nonostante i suoi difetti, è utile
per un controllo sulla sintassi)


b) si richiede una parte di codifica e di testing mediante Dresden, non necessariamente per tutte le classi,
basta una parte del progetto. Ciò richiede lo sviluppo di Drivers e Stubs (messi nel main di una classe o in opportune
classi di testing)


c) Consiglio per lo sviluppo del progetto: concentrare lo sforzo sulla stesura del modello UML e delle specifiche
mediante OCL, usando Argo. Per le unità scelte per il testing è bene dare specifiche dettagliate delle stesse. Solo in una seconda
fase passare allo sviluppo Java, generando il codice da Argo (e modificando eventuali errori dello strumento) in
modo da avere i vincoli scritti correttamente. Se il modello è ben fatto, non dovrebbe accadere di doverlo rivedere se
non per piccole cose, e in questa fase il lavoro è direttamente in Java Dresden.

e..

a) la valutazione è principalmente sul modello UML (quali sono i concetti rilevanti in un modello di agenda,
quali le relazioni fra essi, quali le principali funzionalità) e i vincoli OCL; per questa parte Argo
fornisce un controllo sintattico dei vincoli.


b) Si richiede una parte di codifica in Java e di testing delle unità sfruttando il toolkit di Dresda per gli oracoli. La parte di test
può riguardare un sottoinsieme delle classi, pur di sviluppare stub e drivers di test per le parti non codificate
e necessarie al testing. Se il prodotto della parte a) è ben fatto e stabile, la parte b) non userà più Argo (resteranno
la struttura delle classi ed i vincoli) e sarà solo codifica in Java.


c) Non si valuteranno invece (non influiranno sul voto) aspetti quali una buona interfaccia, uso di grafica, ecc.

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Primo problema l'installazione del toolkit di dresda:
qual è il pacchetto da installare (dalla pagina download di http://dresden-ocl.sourceforge.net/ e la disposizione delle cartelle (ha un path di compilazione simile a java? o in quale directory va compilato?) per far funzionare l'esempio visto a lezione di laboratorio??
forse ho un problema di compatibilità con java: funziona con j2sdk-1.4.2.06 e corrispondente j2re??

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Secondo problema amletico: compilando ed eseguendo col dresden, se il programma crea gli oggetti leggendo da input, al momento dell'inserimento di un valore non valido che viola un vincolo, l'esecuzione del programma termina con l'avviso della violazione.. non dovrebbe esserci un procedura java che in qualche modo cattura la violazione la segnala e permette l'inserimento di un altro valore???

Arcadia82

.consigliere.

User info:

Registered: Sep 2002
Posts: 144 (0.02 al dì)
Location: Canegrate
Corso: Informatica
Anno: secondo
Time Online: 15:57:20 [...]
Status: Offline

Post actions:

Originally posted by picoid82
Secondo problema amletico: compilando ed eseguendo col dresden, se il programma crea gli oggetti leggendo da input, al momento dell'inserimento di un valore non valido che viola un vincolo, l'esecuzione del programma termina con l'avviso della violazione.. non dovrebbe esserci un procedura java che in qualche modo cattura la violazione la segnala e permette l'inserimento di un altro valore???

picoid82

.consigliere.

User info:

Registered: Apr 2003
Posts: 137 (0.02 al dì)
Location: Milano
Corso: Informatica
Anno: 3/4
Time Online: 1 Day, 18:03:43 [...]
Status: Offline

Post actions:

Originally posted by Arcadia82
l'esecuzione del programma termina con l'avviso della violazione.. <<< Vuol dire che hai sbagliato a fare il codice java. Una cosa che sembra che non sia chiara a nessuno è la seguente: i vincoli OCL oltre ad esprimere condizioni inesprimibili in UML servono per il testing, ossia per verificare che certe condizioni vengano rispettate durante l'esecuzione del programma. Se quindi si ottiene una violazione di un vincolo vuol dire che il codice java che hai fatto contiene errori. Un altro suggerimento è il seguente secondo me: i vincoli OCL NON SONO UNA RIPETIZIONE di eventuale codice Java che andremo a fare. Come considerazione sembra banale, però all'inzio i dubbi sorgono spontaneamente. Per rendersene conto basta vedere gli esempi delle fotocopie e del materiale inviato per email.

ok,forse mi son espresso male, facciamo un esempio +"tera-tera":

una classe A con attributo a vincolato in Argo con invariante che a>5, il main della classe mi chiede di dare in input il valore della variabile da assegnare all'oggetto, ok? se il codice java ha come costruttore A oggetto = new A(valore); nel momento in cui dò in input 3 viene segnalata la violazione... termina l'esecuzione ed è chiaro che non dovrebbe succedere..e fin qui ok!
Se però il codice java è ..lettura del valore input... if(valore > 5) A oggetto = new A(valore) else System.out..."valore non valido, reinserire..", allora la domanda è: dove interviene il controllo del vincolo?? dov'è la fase di testing?? cioè il codice java basterebbe da solo, senza commenti creati da argo e senza compilazione col dresden il mio programma crea comunque istanze vincolate (tutto ciò a me sembra proprio una ripetizione, chiedo scusa se è una castroneria! ma non capisco..)

grazie..