Winzipedia: wiki di vincenzomanzoni.com | Informatica3 / JML

Informatica3.JML Versioni

Mostra le modifiche minori - Mostra le modifiche

13/06/2006 ore 15:07 CEST di Giorgio - Integrazione su JML dai lucidi di Gargantini

Modificate le linee 6-7: da:

->[-Introduzione ~~all'~~Java Modeling Language (JML).-]

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

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.

* La versione inglese di [[http://en.wikipedia.org/|Wikipedia]] ha una voce che riguarda [[http://en.wikipedia.org/wiki/JML|JML]].

Ripristina

01/06/2006 ore 21:38 CEST di Vincenzo - 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]].

* [[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]].

Ripristina

01/06/2006 ore 21:35 CEST di Vincenzo - Completamento degli appunti di Giorgio

Modificate le linee 9-10: da:

~~Contenuto della sezione~~.

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.

Ripristina

01/06/2006 ore 21:25 CEST di Vincenzo - 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

Ripristina