cerca
LPS - JML
modifica cronologia stampa login logout

Wiki

UniCrema


Materie per semestre

Materie per anno

Materie per laurea


Help

LPS - JML

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