|
Wiki
UniCrema
Materie per semestre
Materie per anno
Materie per laurea
Help
|
|
Return to LPS - JML ( Edit)
Uni.LPSJML History
Hide minor edits - Show changes to output
Changed lines 1-2 from:
to:
(:titolo LPS - JML:)
%titolo%''':: LPS - JML ::'''
!!Che cos'è JML
JML è un'estensione del linguaggio Java, in esso integrabile sotto forma di commenti ai programmi, che permette l'implementazione dei principi di ''design by contract'' in modo semplice e conciso.
I tipi di espressioni JML sono: Added lines 12-18:
!!Invarianti
Sono quelle condizioni che devono rimanere invariate durante tutta l'esistenza di una classe. Si segnano così:
[@
/*@ invariant <espressione>; *@/
@]
Added lines 292-297:
!!!Esercitazioni
Si trovano, dal laboratorio, su '''Titano''' a questo indirizzo:
[@
\\Titano\Public\Linguaggi di programmazione per la sicurezza
@]
Changed line 235 from:
to:
Added lines 266-291:
!!!jmlc
C'è la versione da linea di comando:
[@
jmlc file.java
@]
produce il '''.class'''. Se ci sono più files, posso fare:
[@
jmlc -Q *.java
@]
Se voglio spostare il file generato da qualche parte:
[@
jmlc -d ../bin file.java
@]
C'è anche un'interfaccia grafica: '''jml-release.jar'''. Permette di selezionare due cose:
* '''jml checker''' = controlla la sintassi ma non genera il .class
* '''jmlc''' = controlla e compila
Dopo aver generato il .class, la si esegue con il '''jmlrac''' che è uno script che fa tutto automatico. Il motivo è che le classi di runtime di JML, contenute in '''jmlruntime.jar''', devono entrare nel classpath di Java. Lo script '''jmlrac''' lo fa in automatico:
[@
jmlrac PersonMain
@]
Il parametro è il nome del .class che contiene il main.
Changed line 262 from:
to:
Altri tools (che non useremo) sono: Changed lines 265-268 from:
* '''jmldoc''': genera documentazione html a partire da espressioni JML to:
* '''jmldoc''': genera documentazione html a partire da espressioni JML
----
[[Torna alla pagina di LPS -> LinguaggiProgrammazioneSicurezza]]
Changed lines 260-265 from:
'''jmlrac''' è l'interprete Java che esegue il controllo di tutte le asserzioni JML, e se non vengono rispettate solleva eccezioni. to:
'''jmlrac''' è l'interprete Java che esegue il controllo di tutte le asserzioni JML, e se non vengono rispettate solleva eccezioni.
Altri tools sono:
* '''escjava2''': controlla staticamente il codice per la prova di correttezza
* '''jmlunit''': fa l'unit test con JML
* '''jmldoc''': genera documentazione html a partire da espressioni JML
Changed lines 253-260 from:
Questo è il costruttore. come invariante di classe, avevamo detto che il campo '''name''' doveva essere diverso dalla stringa vuota, e che il peso doveva essere non negativo. Come precondizione del costruttore, richiediamo che il parametro passato al costruttore, e che servirà per inizializzare proprio '''name''', sia diverso dalla stringa vuota. Inoltre, richiediamo che il riferimento alla variabile n non sia '''null''', tramite l'operatore '''non_null'''. Da notare che il fatto che n sia null e che sia la stringa vuota sono due cose diverse. to:
Questo è il costruttore. come invariante di classe, avevamo detto che il campo '''name''' doveva essere diverso dalla stringa vuota, e che il peso doveva essere non negativo. Come precondizione del costruttore, richiediamo che il parametro passato al costruttore, e che servirà per inizializzare proprio '''name''', sia diverso dalla stringa vuota. Inoltre, richiediamo che il riferimento alla variabile n non sia '''null''', tramite l'operatore '''non_null'''. Da notare che il fatto che n sia null e che sia la stringa vuota sono due cose diverse. Inoltre, specifico in che modo va inizializzato il campo '''name'''.
!!Tool per JML
'''JML compiler''':\\
'''jmlc''' è il compilatore jml: compila i file java e crea dei '''.class''' instrumentati in modo che controllino le asserzioni
'''JML/Java interpreter''':\\
'''jmlrac''' è l'interprete Java che esegue il controllo di tutte le asserzioni JML, e se non vengono rispettate solleva eccezioni.
Changed lines 242-253 from:
Queste condizioni sono molteplici. In particolare, con '''old''' controlliamo che il peso, alla fine del metodo, sia uguale a quello di partenza (che appunto old recupera) a cui è stato sommato il valore di '''kgs'''. to:
Queste condizioni sono molteplici. In particolare, con '''old''' controlliamo che il peso, alla fine del metodo, sia uguale a quello di partenza (che appunto old recupera) a cui è stato sommato il valore di '''kgs'''.
[@
/*@
@ requires !n.equals("");
@ ensures n.equals(name) && weight == 0;
@*/
public Person (/*@ non_null@*/ String n);
}
@]
Questo è il costruttore. come invariante di classe, avevamo detto che il campo '''name''' doveva essere diverso dalla stringa vuota, e che il peso doveva essere non negativo. Come precondizione del costruttore, richiediamo che il parametro passato al costruttore, e che servirà per inizializzare proprio '''name''', sia diverso dalla stringa vuota. Inoltre, richiediamo che il riferimento alla variabile n non sia '''null''', tramite l'operatore '''non_null'''. Da notare che il fatto che n sia null e che sia la stringa vuota sono due cose diverse.
Added lines 1-6:
Tipi di espressioni JML
* invarianti a livello di attributi
* pre e post a livello di segnatura di metodi
* assert all'interno del corpo di un metodo Changed line 170 from:
* le postcondizioni della sottoclasse vengono legate a quelle della superclasse con un '''and''' to:
* le postcondizioni della sottoclasse vengono legate a quelle della superclasse con un '''and''' (eredito le condizioni della superclasse) Changed lines 173-242 from:
Per evitare la specifica della superclasse, si usa la parola chiave '''also'''. to:
Per evitare la specifica della superclasse, si usa la parola chiave '''also'''.
!!!assert
Si può specificare un '''assert''' all'interno del corpo di un metodo.\\
La sintassi è
[@
assert <condizione>;
@]
Esempio:
[@
if (i<=0 || j < 0) {
...
} else if (j < 5) {
//@ assert i > 0 && 0 <= && j < 5;
...
} else {
//@ assert i > 0 && 0 <= && j > 5;
...
}
@]
Gli '''assert''' nelle branch dell''''if''' controllano che le variabili assumano effettivamente il valore che io voglio.
Da Java 1.4 c'è un '''assert''' inserito nel linguaggio, che ha le stesse funzionalità. Ma quello di JML
Ad esempio, per controllare che un array non contenga elementi nulli, con l''''assert''' di Java scriverei:
[@
for (n = 0; n < a.length; n++) assert (a[n] != null);
@]
Con l''''assert''' di JML scriverei invece:
[@
/*@ assert (\forall int i; 0 <= i && i < n; a[i] != null) ;@*/
@]
La stessa espressione è più concisa e delimitata dai '''/*@...@*/'''.
Se compilo attivando il controllo run time, il check dell'assert JML viene eseguito: per fare ciò devo compilare con la flag '''-ea'''.
!!Esempione
[@
public class Person {
private /*@ spec_public non_null@*/ String name;
private /*@spec_public non_null@*/ int weight;
//@ invariant !name.equals("") && weight >= 0;
@// also ensures \result != null;
public String toString();
//@ ensures \result == weight;
public int getWeight();
@]
* '''//@ invariant !name.equals("") && weight >= 0;''' = voglio asserire che il nome non sia la stringa vuota. '''equals''' è un metodo della classe String e serve per verificare l'uguaglianza tra due oggetti (in questo caso stringhe). Inoltre voglio che il peso sia maggiore o uguale a 0.
* '''@// also ensures \result != null;''' = uso '''also''' perché sto overridando il metodo '''toString''', a cui voglio aggiungre l'asserzione qui scritta: il risultato non deve essere null. E' legato alla specifica sull'attributo '''name'''
* '''//@ ensures \result == weight;''' = voglio che il risultato sia uguale a '''weight'''. '''getWeight()''' è un metodo accessorio, che serve per recuperare il valore della variabile private weight. Potrei anche dichiararlo '''pure''' e non forzare, sopra, la '''spec_public'''
[@
(*@
@ requires kgs >= 0;
@ ensures weight == \old(kgs + weight);
@*/
public void addKgs()(int kgs);
@]
Queste condizioni sono molteplici. In particolare, con '''old''' controlliamo che il peso, alla fine del metodo, sia uguale a quello di partenza (che appunto old recupera) a cui è stato sommato il valore di '''kgs'''.
Added lines 132-167:
Sono simili a quelle di Java.
[@
public class Bag {
private int n;
//@ requires n > 0;
public int extractMin() {...}
...
}
@]
Questa roba darebbe errore, perché la pre è relativa ad un metodo '''public''', ma la variabile su cui lavora è '''private'''.
Per risolvere questo problema, uso la dicitura
[@
private /*@ spec public @*/ int n;
//@ requires n > 0;
@]
e in questo modo, posso usare la public n anche per il metodo privato.
In alternativa, posso usare i metodi accessori '''get...()''' (proprietà) dichiarati come '''pure'''. Ad esempio:
[@
public /*@pure@*/ int getN() { return n; }
@]
!!!Ereditarietà
Abbiamo una superclasse sui cui è espressa una specifica. Estendiamo poi questa classe: la classe derivata erediterà anche la stessa specifica JML?
Ecco le regole:
* le precondizioni della sottoclasse vengono legate alle precondizioni della superclasse con un '''or''' disgiunto.
* le postcondizioni della sottoclasse vengono legate a quelle della superclasse con un '''and'''
* anche gli invarianti vengono legati da '''and'''
Per evitare la specifica della superclasse, si usa la parola chiave '''also'''.
Changed lines 117-131 from:
La post ci dice che il valore di n deve essere uguale al vecchio valore di n (indicato con '''\old(n)''' a cui incremento 1. to:
La post ci dice che il valore di n deve essere uguale al vecchio valore di n (indicato con '''\old(n)''' a cui incremento 1.
!!!pure
Le espressioni JML vengono formata a partire da operatori Java più qualche cosa di aggiuntivo. Gli operandi di queste espressioni sono o attributi della classe, o argomenti dei metodi della classe, oppure valori restituiti dai metodi stessi, ma per accedere a questi devo dichiararli come '''pure''', cioè puri. Un metodo puro è tale se è considerato senza side effect, cioè non causa effetti collaterali.
Esempio:
[@
static /*@ pure @*/ int abs (int x) {
if (x >= 0) return x; else return -x;
}
@]
Dichiarandolo '''pure''', dichiaro che '''abs''' può essere usato come operando all'interndo di espressioni JML.
!!!Regole di visibilità
Added lines 83-117:
!!!non_null
Questo operatore serve per asserire che i riferimenti agli oggetti non siano nulli. Serve in diversi punti: attributi e alori di ritorno dai metodi.
Ad esempio:
[@
private /*@ non_null @*/ File[] files;
@]
la posizione di '''non_null''' deve stare appena dopo la visibilità del metodo.
[@
void createSubdir (/*@non_null@*/ String name) {...}
Directory /*@ non_null @*/ getParent() {...}
@]
In questo caso, il '''non_null''' è applicato al valore di ritorno del metodo.
Non ha senso applicare il '''non_null''' a tipi che non siano oggetti, cioè primitivi.
!!!old(VARIABILE)
Si usa per accedere al valore che una variabile aveva PRIMA dell'esecuzione del metodo.
Esempio:
[@
public class Contatore {
int n;
//@ ensures n == \old(n) + 1
public void incrementa() {n ++; }
...
}
@]
La post ci dice che il valore di n deve essere uguale al vecchio valore di n (indicato con '''\old(n)''' a cui incremento 1.
Changed lines 72-82 from:
Il range è '''0 <= i && i< a.length;'''. Voglio verificare che il valore restituito dal metodo sia '''<= a[i]''', ed è la condizione espress da '''\result'''. to:
Il range è '''0 <= i && i< a.length;'''. Voglio verificare che il valore restituito dal metodo sia '''<= a[i]''', ed è la condizione espress da '''\result'''.
Ma questa post è debole: il metodo potrebbe sì restituire un numero inferiore a tutti gli elementi dell'array, ma non appartenente all'array stesso. Per rafforzare la post occorre un doppio quantificatore, che ci dica che l'elemente deve sia essere minore che appartenente all'array: esiste un elementi in a che è uguale a result.
[@
ensures (\forall int i; 0 <= i && i < a.length; \result <= a[i])
&& (\exists int i; 0 <= i && i < a.length; \result == a[i]
@]
Ho aggiunto il quantificatore '''exists''', la cui condizione '''\result == a[i]''' è che l'elemento appartenga all'array.
Changed lines 57-72 from:
Questa roba corrisponde alla scrittura logica ''per ogni s = Student in juniors, tale che s.getAdvisors() è diverso da null''. to:
Questa roba corrisponde alla scrittura logica ''per ogni s = Student in juniors, tale che s.getAdvisors() è diverso da null''.
Altro esempio: abbiamo un metodo che restituisce il minimo elemento di un array. Il metodo si chiama '''int find_min(int[])'''.
Precondizione: l'array a non è null, e contiene almeno un elemento:
[@
requires a != null && a.length >= 1;
@]
E' importante dire che a != null, perché se a fosse null, non saprei nemmeno che cosa restituire.
Postcondizione: l'elemento restituito deve essere effettivamente minore di tutti gli elementi nell'array:
[@
ensures (\forall int i; 0 <= i && i< a.length; \result <= a[i]);
@]
Il range è '''0 <= i && i< a.length;'''. Voglio verificare che il valore restituito dal metodo sia '''<= a[i]''', ed è la condizione espress da '''\result'''.
Added lines 1-57:
!!Precondizioni
Sono precedute da '''requires'''. Esempio:
[@
/*@requires amount >= 0@*/
@]
!!Postcondizioni
Sono segnate con '''ensures'''. Se non ce ne sono, si può scrivere '''ensures true''':
[@
/*@ensures true;@*/
@]
!! Espressioni booleane in JML
Si può usare solo l'operatore '''<==>''' che è il '''se e solo se''' della logica.
Ad esempio, se un metodo restituisce '''true''' solo se '''j < n''', avrei
[@
boolean minore(int j, int n) { return j < n};
@]
Si tratterebbe di una postcondizione JML, e viene scritta così:
[@
//@ ensures \result <==> j < n;
@]
e vuol dire: '''restituisci true se e solo se j è strettamente minore di n'''. Da notare che l'operatore <==> non esiste in Java.
!!!Quantificatori
Esistono i quantificatori
* universali: \forall
* esistenziali: \exists
* generali: \sum \product \min \max
* numerici: \num_of
Per tutti sti quantificatori, la sintassi è:
[@
<quant> <tipo> <var>; <range predicate>; <espressione>
@]
dove
* var è la variabile che uso per scansionare la collezione di oggetti (iteratore)
* range predicate è il predicato che deve essere soddisfatto per gli elementi della collezione
Ad esempio, possiamo volere che tutti gli oggetti contenuti nella Collection '''juniors''' abbiano un '''advisor''', che viene ottenuto dal metodo getAdvisor().\\
In JML scriverei quindi:
[@
(\forall Student s; juniors.contains(s); s.getAdvisor() |= null)
@]
* '''\forall Student s;''' = quantificatore, tipo, variabile
* '''juniors.contains(s);''' = range predicate
* '''s.getAdvisor() |= null''' = espressione
Questa roba corrisponde alla scrittura logica ''per ogni s = Student in juniors, tale che s.getAdvisors() è diverso da null''.
|
|
