Specifiche senza JML: uso delle
asserzioni
Asserzioni in Java
• Dal jdk 1.4 (da Febbraio 2002) c’è meccanismo per gestire asserzioni
• Asserzione: espressione booleana da verificare a run-time
– se espressione è vera allora si continua
– se espressione è false sistema genera errore: AssertionError, non recuperabile, e
il programma termina
• Asserzioni possono essere abilitate (o lasciate disabilitate) in fase di
compilazione (tipico: si usano durante testing, si disabilitano al rilascio):
– javac –source 1.4 Myclass.java
se codice contiene asserzioni:
– java –source 1.4 –ea Myclass.java
In sistemi safety-critical spesso le asserzioni sono lasciate abilitate anche sul
campo (ma in in modo da non causare la terminazione del programma)
• Sintassi: assert <espressione boolena>;
• Asserzioni possono essere usate ad esempio per verificare le postcondizioni
– in certi casi anche per precondizioni di metodi private, allo scopo di testing. In
Java non si usano asserzioni per le precondizioni dei metodi pubblici
2
Verifica postcondizione
• Se ensures è verificabile facilmente, si può inserire asserzione:
• static int search(int a[], int x) {
//@requires (* a <> null *)
//@ensures (*se x è presente in a ne restituisce la posizione
// altrimenti restituisce –1*)
int i;
… //qui si cerca x in a, memorizzandone posizione in i
assert(i == -1 || a[i] = =x);
return i;
}
• Es: se asserzioni abilitate e procedura trova i che non corrisponde a x 
AssertionError
• NB: in questo caso la condizione in assert è più debole della
postcondizione!
3
Dettagli per assert e AssertionError
Per avere informazioni sull’asserzione fallita, si può usare sintassi
assert Expression1 : Expression2 ;
•
•
Expression2 può essere di tipo primitivo o di tipo Object e contiene il
messaggio dettagliato mostrato dal costruttore di AssertionError quando
l’asserzione Expression1 fallisce
Esempi:
•
•
•
static int search(int a[], float x) {
… …//codice che esegue la ricerca
assert (i ==-1 || a[i] = =x) : “search(int[], float) non mantiene
postcomd.:” + i ;
return i;
}
AssertionError()
Constructs an AssertionError with no detail message.
...
AssertionError(Object detailMessage)
Constructs an AssertionError with its detail message derived from the specified
object, which is converted to a string
4
Implementare RI
il rep invariant definisce tutte le ipotesi sottostanti
all’implementazione di un tipo
– definisce quali rappresentazioni sono legali (true), cioè per quali valori
AF è definita
– deve essere verificato in tutti gli stati osservabili dagli utilizzatori
– si implementa con metodo repOk():
• Qualora non si riesca a scriverlo in un JML eseguibile è anche
possibile implementarlo in Java con un metodo ad hoc, detto
repOk():
public boolean repOk() {
// EFFECTS: restituisce true se rep invariant vale per this,
//
altrimenti restituisce false
...}
5
Esempio: repOk per IntSet
public boolean repOk() {
// c.els <> null && :
if (els == null) return false;
//for all integers i. (0 <= i < c.els.size => c.els[i] è un Integer != null) && :
for (int i = 0; i < els.size(); i++) {
Object x = els.get(i);
if (x== null || !(x instanceof Integer)) return false;
//for all integers i, j. (0 <= i< j<c.els.size => c.els[i].intValue !=c.
//els[i].intValue:
for (int j = i+1; j< els.size(); j++)
if (x.equals(els.get(j))) return false;
}
return true;
}
6
Come verificare RI con repOk
1. Nel codice: inserire il controllo di repOk nei mutators e nei
costruttori, tramite il meccanismo delle asserzioni
•
•
Si chiama assert repOk(); al termine del metodo o del costruttore: se
risultato è true si continua, altrimenti AssertionError
Molto utile (ma codice più lento!). Esempio per IntSet:
public void insert(int x) {
… …//codice che inserisce in this.els
assert repOk();
return;}
Se repOk() non è verificato, viene generato errore:
AssertionError in function IntSet.insert(int)
•
NB: per usare assert si deve compilare in Java con la
direttiva apposita
7
Esempio di verifica di repOk() e di
ensures
public void insert(int x) {
//@ensures this.isIn(x) && (*this include gli elementi in \old(this)*)
…//codice che inserisce in this.els
assert repOk() : “insert(int) non mantiene RI:”+ x;
assert isIn(x) : this+ “insert (int) non mantiene postcond:”
+ x;
return;
}
8