.dsy:it. (http://www.dsy.it/forum/)
- Didattica in generale (http://www.dsy.it/forum/forumdisplay.php?forumid=115)
-- [Metodi Formali dell'informatica 1 e 2] Diario del corso 04/05 (http://www.dsy.it/forum/showthread.php?threadid=13506)

[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
  

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

orario concordato

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.

lezione 29/09

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.

lezioni 4/5/6 ottobre

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

lezioni 11/12/13 ottobre

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.

lezioni 18/19/20 ottobre

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

lezioni 25/26/27

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

lezioni varie

- 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

AVVISO

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..

lezioni successive primo modulo

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..

progetto agenda

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.

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??

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???

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???

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.

Originally posted by picoid82
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..

Bene...
1) ho fatto lo schema uml con i relativi vincoli ocl
2) ho scritto il codice java e provandolo a mano sembra funzionare
3) ho iniettato i vincoli ocl con dresden e la compilazione e' andata a buon fine
4) lancio il mio programma ma i vincoli ocl sembrano essere impazziti: ad esempio ho un vincolo sull'ora sulla classe Ora ( ad esempio che il campo ora sia compreso tra 0 e 23 estremi inclusi ), a questo punto creo un oggetto di tipo Ora in cui l'ora è compresa tra 0 e 23. Ecco l'uoutput del mio programma inserendo l'ora 11:00:

Inserire il numero dell'ora:
11
Inserire il numero dei minuti:
0
violated ocl invariant 'ora' on object '0:0'.

A fronte di tale violazione cmq il mio programma non termina e se chiedo di visualizzare l'appuntamento creato esso mi visualizza:

Appuntamento il giorno 1 -1-2004 inserita nota eeeee dalle ore 10:0 alle ore 11:0

Siccome questo è un vincolo semplice e non trovo alcun errore è ovvio che vi sia un baco di Dresden.
Inoltre questo non è l'unico vincolo che risulta dare anomalie di questa tipologia...
A questo punto mi è anche impossibile produrre delle classi di test...
Pertanto chiedo se sia possibile avere un orale in cui si espone il progetto svolto di modo da motivare evetuali parti incomplete... insomma... non sarò un esperto di ocl ma mi pare di avere capito bene il suo funzionamento e come si fa ad esprimere i vincoli in linguaggio ocl stesso: se gli strumenti non funzionano a dovere la cosa non deve influenzare il voto che dovrebbe basarsi sulla mia conoscenza di ocl, a maggior ragione che cmq il progetto l'ho svolto.

Vorrei sapere se è possibile fissare una data per la visione dei progetti oppure se occorre contattare direttamente per email il prof. Ornaghi per fissare il colloquio sull'orale.

Domani (10 gennaio) che cosa fate???
Ci troviamo all'orario di lezione magari mandando prima una mail a Trentini??
Ditemi voi..

ciao

Io vorrei fare direttamente l'orale-discussione progetto con Ornaghi, credo oramai di essere saturo di ocl e tool vari

Originally posted by Arcadia82
Io vorrei fare direttamente l'orale-discussione progetto con Ornaghi, credo oramai di essere saturo di ocl e tool vari

Originally posted by picoid82
ma hai scritto al professore chiedendo se esiste questa forma di valutazione? o basta solo la consegna?

ps. tornando al progetto mi dici come metti le directory per compilare col dresden-ocl-injector? devo mettere i *.java nella cartella dove c'è injector o no??

Per quelli che mi chiedono l'indirizzo di download: http://sourceforge.net/project/show...lease_id=128589

qui c'è la versione 1.1, è giusta vero??

grazie

Per la compilazione... allora... innanzi tutto supponiamo di essere nella directory Agenda. In tale directory ho il file agenda.zargo. A questo punto da ArgoUml dico che tutte le classi generate faranno parte del package denominato test (a voi le fatiche per scoprirlo?! Ci ho perso una giornata...). Bene a questo punto genero il codice java da ArgoUml IL QUALE MI CREA DA SOLO LA DIRECTORY test in Agenda in quanto ho detto che tutte le classi sono del package test...
A questo punto dalla directory Agenda a linea di comando lancio:
1) Per iniettare i vincoli:
java -jar dresden-ocl-injector.jar -m -r test test/*.java
2) Per compilare:
javac -classpath dresden-ocl-injector.jar test/*.java
3) Per eseguire (se il main lo avete in Agenda.java):
java -classpath dresden-ocl-injector.jar test/Agenda
4) Se devo ritoccare il codice java prima di riaprire i relativi file .java li pulisco dai vincoli ocl tramite:
java -jar dresden-ocl-injector.jar -m -c test/*.java

Bon... spero di averti dato un po di aiuto. [/B]

Originally posted by picoid82
ci ho sbattuto la testa per ore ma ho in parte risolto...

a me funziona solo se la directory test o comunque quella creata da ARGO col nome del package è contenuta come sotto directory del dresden, ovvero sotto o allo stesso livello dell'injector..
magra consolazione, ma almeno funziona!!