2. JML

Le specifiche in JML vanno racchiuse in commenti in uno dei seguenti modi:

// @ ...

oppure

/* @ ...
@ ...
@ ...
@*/

Asserzioni

Sono delle espressioni booleane.

Requires e Ensures

//@ requires in >= 0;
//@ ensures Math.abs(\result * \result-in)<0.0001;
public static float sqrt (float in);

requires specifica le precondizioni, ensures specifica le postcondizioni, \result indica il valore prodotto alla fine dell’esecuzione del metodo.

Commenti

(* questo è un commento *)

Assignable

Permette di specificare quale parametro può essere modificato dal metodo.

In questo metodo l'array a può essere modificato.

//@assignable a[*];
//@ ensures (* a is a permutation of the original value of a*)
//@ && (* a is sorted by increasing values *)
public static void sort (int[] a)

Se un metodo non modifica nessuna variabile si scrive aggignable \nothing.

In questo metodo nessuna variabile viene modificata.

//@ assignable \nothing;
//@ ensures (*x is in a*) && x==a[\result]
//@ || (* x is not in a *) && \result ==-1;
public static int search (int[ ] a, int x)

Se la clausola assignable viene omessa, tutte le variabili coinvolte nel metodo possono essere modificate.

Eccezioni

Si utilizza la clausola signals per segnalare delle eccezioni che possono essere lanciate dal metodo.

//@ assignable \nothing;
//@ ensures x == a[\result];
//@ signals (NotFoundException e) (* x is not present in a *);
public static int searchs(int x, int [] a) throws NotFoundException

Significato:

• se la postcondizione è verificata, il metodo ritorna il valore calcolato

• se la clausola signals è verificata, il metodo lancia l’eccezione specificata da signals.

Per ogni eccezione che può essere lanciata dal metodo, è necessario scrivere una clausola signals.

Precondizioni o eccezioni?

Una procedura è parziale se possiede una precondizione non vuota: la precondizione fa sì che il metodo segua il comportamento specificato solo per un insieme ristretto di valori del dominio che la variabile può assumere.

Questo rende il metodo unsafe, poiché per valori che non rispettano le precondizioni, accettiamo qualsiasi comportamento da parte del metodo chiamata: questa è una cosa pericolosa per il programma.

Una procedura dovrebbe essere pertanto totale (non parziale).

Quando si ha a che fare con dei metodi pubblici di classi pubbliche, non specifichiamo la clausola requires, ma lanciamo un’eccezione ogni volta che la precondizione del metodo viene violata. Così facendo evitiamo comportamenti potenzialmente distruttivi per il programma.

Versione da EVITARE:
//@ requires x != null;
//@ ensures a[\result].equals(x);
//@ signals (NotFoundException e) (*x is not in a *);
public static int search(String x, String[] a) throws NotFoundException

Versione da SEGUIRE:
//@ ensures x != null && a[\result].equals(x);
//@ signals (NotFoundException e) (*x is not in a *)
//@ signals (NullPointerException e) x == null;
public static int searchs(String x, String[] a) throws NullPointerException, NotFoundException

Quantificatori

Per parlare degli elementi delle collezioni è possibile usare i seguenti metodi:

• equals

• contains

• containsAll

• get

• sublist(<initial_position>, <final_position>)

• size

//@ ensures a.containsAll(\old(a.sublist(0,a.size())) &&
//@ \old(a.sublist(0,a.size()). containsAll(a)
//@ && (* to sorted by increasing values*);
public static void sort (ArrayList<Integer> a)

Forall: quantificatore universale. La sintassi è (\forall <variable>; <range>; <condition>), la semantica è “per tutti i valori che soddisfano range, condizione deve essere true”.

(\forall int i; 0<=i && i< a.length-1; a[i]<=a[i+1])

Exists: quantificatore esistenziale.

(\exists int i; 0<=i && i< a.length;a[i] == x)

Num_of: la sintassi è (\num_of int i; P(i); Q(i)) e ci ritorna il numero di i che rendono vere P(i) e Q(i).

(\numof int i; 0<=i&& i< a.length; a[i]>0)

Altre operazioni:

(\sum int i; 0 <= i && i < 5; i+1)    // == 1 + 2 + 3 + 4+5
(\product int i; 0 < i && i < 5; i*i) // == 1 * 4 * 9 * 16
(\max int i; 0 <= i && i < 5; i*i)    // == 16
(\min int i; 0 <= i && i < 5; i-1)    // == -1