:: 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:
- invarianti a livello di attributi
- pre e post a livello di segnatura di metodi
- assert all'interno del corpo di un metodo
Invarianti
Sono quelle condizioni che devono rimanere invariate durante tutta l'esistenza di una classe. Si segnano così:
/*@ invariant <espressione>; *@/
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.
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.
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.
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.
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à
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 (eredito le condizioni della superclasse)
- anche gli invarianti vengono legati da and
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.
/*@
@ 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. 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.
Altri tools (che non useremo) 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
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.
Esercitazioni
Si trovano, dal laboratorio, su Titano a questo indirizzo:
\\Titano\Public\Linguaggi di programmazione per la sicurezza
Torna alla pagina di LPS
