3. ADT

Solo gli elementi pubblici di un metodo o di una classe possono comparire nella specifica JML di un metodo pubblico e non statico: in particolare possono comparire parametri formali del metodo, \result, attributi pubblici e metodi puri pubblici.

NB: i metodi pubblici che non sono stati dichiarati come puri NON possono essere inclusi nella specifica.

I metodi puri sono metodi non statici dichiarati con la parola chiave JML pure. Questi sono metodi che non hanno effetti collaterali.

Esempio di metodo puro:

//@ ensures (*\result is cardinality of this *) 
public int /* @ pure */ size(){}

I metodi puri permettono di osservare lo stato di un oggetto.

Specificazione dell’astrazione dei dati

Esempio: si vuole realizzare un insieme di interi (IntSet).

I valori possibili sono tutti i possibili insiemi di interi, con una qualsiasi cardinalità, senza elementi ripetuti.

public class IntSet {
// OVERVIEW: unlimited and modifiable sets of integers; //e.g.: {1, 2, 10, -55}

//observers:
//@ ensures result == (*x is among the elements of this*);
public /*@ pure @*/ boolean isIn (int x){} 

//@ ensures (*\result is cardinality of this *);
public /*@ pure @*/ int size(){}

//@ ensures this.isIn(\result) && this.size()>0; 
//@ signals (EmptyException) this.size()==0;}
public /*@ pure @*/ int choose() throws EmptyException {}

//constructors:
//@ensures this.size()==0;
public IntSet(){// initialize this as an empty set }

//mutators:
//@ ensures this.isIn(x) && size()=\old(size() + \old(isIn(x) ? 0 : 1) && 
//@ (\forall int y; x!=y; \old(isIn(y)) <==> isIn(y));
public void insert(int x){ //inserts x into this }

//@ ensures !this.isIn(x) && size()=\old(size() - \old(isIn(x) ? 1 : 0) &&
//@ (\forall int y; x!=y; \old(isIn(y)) <==> isIn(y));
public void remove(int x){//removes x from this
}

In questo esempio vengono definiti metodi appartenenti a 3 categorie:

Uso di Abstract Data Types

La specifica deve essere sufficiente a permettere l’uso dell’astrazione, senza saperne l’implementazione.

Classe pura

Tutti i suoi metodi non statici e i costruttori vengono definiti come puri.

Specifica formale delle collezioni

In generale, lo stato concreto di un oggetto appartenente ad una classe non è visibile (spesso gli attributi sono privati): per questo motivo lo stato di un oggetto non deve essere usato nelle specifiche.

Dall’altra parte, lo stato astratto può essere osservato mediante i metodi observer, e quindi può essere usato nelle specifiche.

Però i metodi observer spesso non sono sufficienti a descrivere le condizioni delle specifiche, siccome non catturano completamente lo stato di un oggetto… questo spesso accade con le collezioni.

Per questo motivo si usano nelle specifiche gli OAT (Typical Abstract Object): generalmente è una List, String o Set.

// Esempio
public class Stack<T> {

//@public List<T> oat;
//@ Typical object oat is [x_0, x_1, ..., x_n], n>=0, x_i in T, x_n is the top

//@ensures \result == oat.size(); 
public /*@ pure @*/ int size(){ ... }

//@requires size()>0;
//@ ensures \result== oat.get(size()-1);
public /*@ pure @*/ T top() throw EmptyException;

//@ ensures size()==0; 
public Stack() { ... }

//@ensures size()==\old(size()+1)&&top()==x &&
//@ \old(oat.sublist(0,size())).equals(oat.sublist(0,size()-1)); 
public void push(T x) {...}

//@requires size()>0;
//@@ensures size()===\old(size()-1)&& oat.equals(\old(oat.sublist(0, size()-1)) 
public void pop(){...}
}

Categorie di operazioni

Creators: producono un nuovo oggetto.

Producers: dati in input oggetti del proprio tipo, creano oggetti del proprio tipo.

Modifiers ( o Mutators): modificano un oggetto del proprio tipo

Observers: dati in input oggetti del proprio tipo, ritornano cose di altri tipi

Adeguatezza di un tipo

Un tipo è adeguato se fornisce un numero sufficiente di operazioni per il tipo, in modo tale da farne uso in modo semplice ed efficiente.

Condizioni di verifica:

Proprietà astratte

Sono osservabili con metodi pubblici.

Ci sono due categorie:

Solo le proprietà invarianti sono rappresentabili in JML.

Invarianti

Ignoriamo l’implementazione ed usiamo solo la specifica per descrivere gli invarianti, che sono formalizzazioni di una proprietà astratta.

Un invariante è una condizione che deve essere sempre verificata da ogni oggetto astratto.

Devono essere derivabili dalla specifica dei motodi di una classe.

In JML vengono scritti come public invariante possono solo utilizzare attributi e metodi pubblici di una classe.

//@ public invariant this.size()>=0
//@ public invariant this.degree()>=0;

Gli utilizzatori di una classe possono sfruttare le proprietà come assunzioni riguardo al comportamento di una classe.

Affinché esse siano utili, è necessario essere sicuri che gli invarianti vengano verificati: scrivere un invariante non è sufficiente a garantire che esso sia vero… deve essere una conseguenza di una specifica di un metodo.

Oggetti astratti vs. oggetti concreti

La specifica di un’astrazione definisce oggetti astratti.

L’implementazione della specifica definisce oggetti concreti.

Esempio: nel caso di prima l’insieme di interi è l’oggetto astratto, IntSet è l’oggetto concreto.

Ogni cambiamento al codice può modificare l’oggetto concreto, ma deve lasciare intatto l’oggetto astratto.

Implementazione di un’Abstract Data Type

L’implementazione di un tipo deve fornire:

Data la stessa struttura dati, la scelta della rappresentazione usata aper contenere i dati può avere effetti sull’efficienza.

Lo stato astratto viene definito dalla specifica, quello concreto viene definito dalla rappresentazione scelta per immagazzinare i dati.

Funzione di Astrazione (AF)

Associa ogni stato concreto ad al più uno stato astratto: definisce il significato della rappresentazione scelta in fase di implementazione.

Come si definisce quindi un’AF? Con un invariante:

Una funzione di astrazione descrive come l’oggetto concreto memorizza l’informazione di un oggetto astratto.

Si può specificare con un invariante privato, che mette in relazione attributi privati e observers pubblici.

Di solito viene implementate con la funzione toString(), che non è definita per gli oggetti “illegali”.

Oggetti Legali e Illegali

Non tutti gli oggetti concreti sono legali: come faccio a sapere se un oggetto lo è o no?

Rappresentazioni legali di un oggetti sono quelle per le quali tutte le assunzioni fatte a riguardo dell’implementazione sono verificate.

Invariante di rappresentazione (RI)

È un predicato vero solo per le rappresentazioni legali di un oggetto.

Esempio: un RI per un oggetto concreto di IntSet è:

In JML:

//@ private invariant els != null && 
//@ !.els.contains(null) &&
//@ (\forall int i; 0 <= i && i<els.size(); 
//@ (\forall int j; i <j && j<els.size(); 
//@ !(els.get(i).equals(els.get(j))));

Gli RI fanno riferimento SOLO ad attributi privati di una classe: il rapporto tra oggetti astratti (public) e concreti (private) vengono definiti dalle AF.

Validità di RI

Se un metodo è observer, allora non può modificare il RI.

Un RI deve essere valido negli stati osservabili da un utilizzatore della classe:

Quando scrivere e verificare gli invarianti

Quando si scrive codice: l’implementazione deve essere scritta in un modo che preserva gli RI.

Durante la fase di testing: i programmi di test possono usare gli RI per verificare se un’implementazione è corretta rispetto alla rappresentazione scelta.

Implementazione dei RI

Gli RI definiscono tutte le assunzioni fatte riguardo a un tipo di implementazione:

public boolean repOk() {
// ensures: returns true if rep invariant holds for this,
// otherwise returns false
}

Come verificare RI con repOK

Nel codice si inserisce il controllo di repOK nei mutators e nei constructors, tramite il meccanismo delle asserzioni:

// Esempio
public void insert(int x) {
//@ensures this.isIn(x) && (*this includes the elements in \old(this)*)
... //code inserting into this.els
assert repOk() : "insert(int) does not keep RI: " + x;
assert isIn(x) : this + "insert (int) does not hold postcond:" + x; return;
}

Validità di un’ADT

Per verificare se l’implementazione di un’ADT è corretta si:

  1. Si mostra che l’implementazione rispetta i RI
  1. Si mostra che tutte le operazioni sono corrette rispetto alle specifiche astratte

Validità di un RI

  1. Mostrare che i costruttori ritornano oggetti che rendono veri gli RI, cioè verificare che i costruttori producano oggetti legali
  1. Mostrare che i metodi non helper mantengano vero l’invariante

Esposizione del rep

Un’astrazione mutabile deve avere un rep mutabile: è possibile che il rep cambi anche se l’oggetto astratto non cambia.

Un’implementazione espone il rep quando fornisce agli utenti degli oggetti un modo per accedere a parti mutabili del rep: questo è un grave errore.

Ciò avviene in due modi:

Esposizione del rep con return

Esempio:

// Sia dato il metodo della classe IntSet
//@ ensures (* resituisce un ArrayList con tutti gli elementi in this senza ripetizioni e in ordine arbitrario*)
public ArrayList<Integer> allEls(){
	...
	return els
}

Facendo così gli utenti possono chiamare allEls() e accedere all’implementazione: possono ad esempio inserire elementi duplicati e distruggere il RI. 

// Codice che potrebbe essere usato dall'utente, che andrebbe a distruggere il RI
ArrayList<Integer> v = o.allEls();
v.add(new Integer(4));
v.add(new Integer(4));

// Così ho inserito due copie di 4

In questo caso la soluzione corretta è restituire una copia di els: return els.clone();.

Esposizione del rep da parametro in input

Esempio:

//@ ensures (* this è l'insieme di tutti gli Integer in elms*)
//@ signals (NullPointerException e) elms == null;
public IntSet(Arraylist elms) throws NullPointerException{
	if(elms == null) {
		throw new NullPointerException("Intset 1 argum. contructor");
	}
	els = elms; // ERRATO!!
}

Nel rep viene memorizzato un riferimento ad un oggetto esterno, esponendo il rep.

Così facendo è possibile chiamare il costruttore fornendogli come parametro un ArrayList che contiene duplicati, distruggendo così il RI della classe IntSet, che non prevede elementi duplicati al suo interno.

Come non esporre il rep