|
Categorie
Winzipedia Uso dell'wiki |
JMLInformatica3.JML VersioniNascondi le modifiche minori - Mostra le modifiche Modificate le linee 2-4: da:
'''Autori:''' [[Profiles.Giorgio|Giorgio Ghisalberti]],[[Profiles.Vincenzo|Vincenzo Manzoni]] '''Hanno contribuito:''' a:
'''Autori:''' [[Profiles.Giorgio|Giorgio Ghisalberti]],[[Profiles.Vincenzo|Vincenzo Manzoni]] Modificata la linea 2: da:
'''Autori:''' [[Profiles.Vincenzo|Vincenzo Manzoni]]\\ a:
'''Autori:''' [[Profiles.Giorgio|Giorgio Ghisalberti]],[[Profiles.Vincenzo|Vincenzo Manzoni]]\\ 13/06/2006 ore 15:07 CEST
di - Integrazione su JML dai lucidi di Gargantini
Modificate le linee 6-7: da:
->[-Introduzione a:
->[-Introduzione al Java Modeling Language (JML).-] Aggiunte le linee 9-10:
JML l'acronimo di '''Java Modelling Language'''. E' un insieme di tool e tecniche per il design by contract in Java. Modificate le linee 12-21: da:
Per far questo, si inseriscono all'interno dei file sorgente delle '''annotazioni''' all'interno dei commenti. Le annotazioni sono della forma @@/*@ ... @*/@@ oppure @@ //@ @@ Esistono variabili e operatori appositi, ad esempio @@<==>@@. !!I tool Per JML esistono vari tool: * JML Compiler (@@jmlc@@) * JML/Java Interpreter a:
Per far questo, si inseriscono all'interno dei file sorgente delle ''annotazioni'' all'interno dei commenti nel file .java. Le annotazioni sono della forma @@/*@ ... @*/@@ oppure @@ //@ @@ @@\result, \forall, \old, <==>@@(se e solo se), ... e alcune parole chiave @@\requires, \ensures, \invariant,@@... !!!Pre & Postconditions Ecco un esempio di Precondizione per un metodo: /*@ requires amount >= 0; ensures balance == \old(balance) -- amount && \result == balance; @*/ public int withdraw(int amount) { ... In questo caso @@\old(balance)@@ si riferisce al valore di balance prima dell'esecuzione del metodo. !!!non null Molti elementi all'interno delle pre e delle postcondizioni spesso devono essere non nulli. L'operatore ''non null'' serve proprio per questo motivo. public class Directory { private /*@ non null @*/ File[] files; void createSubdir(/*@ non null @*/ String name){ ... } !!!Assert if (i <= 0 || j < 0) { ... } else if (j < 5){ //@ assert i > 0 && 0 < j && j < 5; ... } else { //@ assert i > 0 && j > 5; ... } !!!Quantificatori JML supporta varie forme di quantificatori: * Universali ed esistenziali (@@\forall e \exists@@) * Quantificatori generali (@@\sum, \product, \min, \max@@) * Quantificatori numerici (@@\num\_of@@) !!Benefici di JML !!Tools per JML # JML compiler (''jmlc''): compila file java per avere class instrumentati # JML/Java interpreter (''jmlrac''): # Controllo statico esteso attraverso escjava2 # JML/JUnit unit test tool (''jmlunit'') # HTML generator (''jmldoc'') # Altri tool Modificate le linee 74-77: da:
* La versione inglese di [[http://en.wikipedia.org/|Wikipedia]] ha una voce che riguarda [[http://en.wikipedia.org/wiki/JML|JML]] !! Da fare # Integrare con le slide di Gargantini quando le ; questo articolo l'ho scritto prendendo le informazioni dagli appunti di Giorgio a:
* La versione inglese di [[http://en.wikipedia.org/|Wikipedia]] ha una voce che riguarda [[http://en.wikipedia.org/wiki/JML|JML]]. 01/06/2006 ore 21:38 CEST
di - Aggiunta dell'homepage di JML
Modificate le linee 21-22: da:
La versione inglese di [[http://en.wikipedia.org/|Wikipedia]] ha una voce che riguarda [[http://en.wikipedia.org/wiki/JML|JML]]. a:
* [[http://www.cs.iastate.edu/~leavens/JML/index.shtml|Homepage di JML]] * La versione inglese di [[http://en.wikipedia.org/|Wikipedia]] ha una voce che riguarda [[http://en.wikipedia.org/wiki/JML|JML]]. 01/06/2006 ore 21:35 CEST
di - Completamento degli appunti di Giorgio
Modificate le linee 9-10: da:
a:
L'idea quella di utilizzare Java non solo per programmare, ma, aggiungendo al linguaggio dei tool e delle tecniche, anche per modellare. Per far questo, si inseriscono all'interno dei file sorgente delle '''annotazioni''' all'interno dei commenti. Le annotazioni sono della forma @@/*@ ... @*/@@ oppure @@ //@ @@ Esistono variabili e operatori appositi, ad esempio @@<==>@@. !!I tool Per JML esistono vari tool: * JML Compiler (@@jmlc@@) * JML/Java Interpreter !! Risorse esterne La versione inglese di [[http://en.wikipedia.org/|Wikipedia]] ha una voce che riguarda [[http://en.wikipedia.org/wiki/JML|JML]]. Aggiunta la linea 24:
# Integrare con le slide di Gargantini quando le ; questo articolo l'ho scritto prendendo le informazioni dagli appunti di Giorgio. 01/06/2006 ore 21:25 CEST
di - Creazione della pagina
Aggiunte le linee 1-11:
!Java Modeling Language (JML) '''Autori:''' [[Profiles.Vincenzo|Vincenzo Manzoni]]\\ '''Hanno contribuito:''' ->'''Sommario''' ->[-Introduzione all'Java Modeling Language (JML).-] !!Introduzione Contenuto della sezione. !! Da fare |