04/06/2014
Estensioni
Estensioni pure
Estensione e' il termine java per ereditarietà :
Un estensione C' di una classe C è un erede di C
Un estensione è detta pura se non modifica la
specifica dei metodi ereditati
Un estensione pura può quindi solo estendere la
specifica, aggiungendo nuove operazioni...
...tuttavia può modificare (a parità di specifica)
l implementazione dei metodi ereditati
altrimenti è detta non pura
2
1
04/06/2014
Estensione pura MaxIntSet: Specifica
Estensione di IntSet, che aggiunge solo il metodo per estrarre
il massimo elemento.
Specifica di tutti gli altri metodi è inalterata.
Costruttore non e' ereditato, quindi potrebbe cambiare.
public class MaxIntSet extends IntSet {
// OVERVIEW: MaxIntSet è sottotipo di IntSet con metodo max per
//estrarre il massimo elemento
//@ensures (*inizializza this come il MaxIntSet vuoto*)
\public MaxIntSet
//@ ensures this.size()>0 &&\result == (\max int i; this.isIn(i);i);
//@signals(EmptyException) this.size() == 0;
public int /* pure */ max() throws EmptyException { }
La specifica di MaxIntSet assume come data la specifica di IntSet
Aggiunge solo ciò che è nuovo (max() e costruttore)
3
MaxIntSet: Implementazione
Per migliorare efficienza, si memorizza il max elemento => occorre reimplentare
tutti i metodi modificatori, anche se specifica non è cambiata! RI cambia.
public class MaxIntSet extends IntSet {
private int biggest;//memorizza il max. Non definito per this=vuoto.
public MaxIntSet(){ super(); }
public int max() throws EmptyException {
if (size() == 0) throw new EmptyException( MaxIntSet.max );
return biggest;
}
@Override
public void insert(int x){
if (size() == 0 || x>biggest) biggest = x;
super.insert(x); //chiama metodo insert di IntSet
}
overriding (ridefinizione)
@Override
public void remove(int x){
super.remove(x);
if(size()==0||x<biggest) return;
(for Iterator<Integer> g: IntSet) {Integer z=g; if(z>biggest) biggest=z;}
}
4
2
04/06/2014
AF e RI?
AF di sottoclasse di solito è uguale a quella della sovraclasse
AF di MaxIntSet è identica a AF di IntSet: MaxIntSet utilizza ancora IntSet per
memorizzare gli elementi.
// la funzione di astrazione è:
//AF_MaxIntSet(c) = AF_IntSet(c)
Rep invariant della classe base è ereditato senza possibilità di modifica e si
aggiunge (in JML con also ) un nuovo RI:
// il rep invariant RI_MaxIntSet(c) è:
//@ also
//@ private invariant this.size>0 ==>
//@ isIn(biggest) && biggest = (\max int x; isIn(x);x);
NB: RI è sempre vero ad esempio quando this è l insieme è vuoto. In tal caso,
biggest può assumere un valore qualunque.
Valgono le consuete regole di visibilità. RI di una estensione può usare:
tutti gli attributi e metodi puri (anche private) definiti nella classe stessa;
attributi e metodi puri ereditati, purche' pubblici o protected.
Quindi se els è private non si può scrivere, al posto dell'ultima linea:
(\forall int i; 0<= i && i<this.size(); els.get(i) <= x)
5
Estensioni non pure
E modificata la specifica di uno o più metodi ereditati
Es. un insieme ordinato SortedIntSet
public class SortedIntSet extends IntSet {
public SortedIntSet {super();}
@Override
//@ ensures (*restituisce un iteratore su tutti e soli gli elementi
di //@this , ciascuno una sola volta, in ordine crescente *);
}
}
NB: Le estensioni non pure di classi concrete andrebbero evitate o
quantomeno limitate (la reimplementazione di metodi sempre
«pericolosa»).
3
04/06/2014
PRINCIPIO DI SOSTITUZIONE
DI LISKOV
Richiami: Open-closed principle
Nei linguaggi a oggetti, è possibile definire astrazioni, tramite
classi (tipicamente classi astratte o interfacce), da richiamare
poi in altri moduli.
Un modulo è chiuso rispetto alla modifica perché la
definizione delle astrazioni non cambia
Ad esempio disegnaTutto() nell editor grafico era definita in base alla
classe astratta Figura. La disegnaTutto non deve più essere modificata.
Le classi però possono essere estese, tramite sottoclassi: ciò
rende un modulo aperto per l'estensione:
definire una nuova classe dalle astrazioni può modificare il
comportamento di un modulo.
Ad esempio disegnaTutto() diventa in grado di disegnare anche trapezi,
ecc.
8
4
04/06/2014
Estendibilità tramite ereditarietà è garantita solo se possiamo
usare oggetti di una classe che sono sostituibili a quelli della
sopraclasse.
Gli oggetti della sottoclasse devono rispettare il contratto della
superclasse
Ad esempio, la disegna() deve contenere codice che disegna l oggetto
this sullo schermo. Ogni sottoclasse di Figura deve definire una
disegna() che abbia lo stesso effetto!
Ma se si definisse disegna() in modo diverso? Ad esempio, se disegna()
di Trapezi fosse definita in modo che disegna this solo se l area e
maggiore di 20? Va ancora bene?
Come fare a garantire che il contratto della superclasse sia
rispettato?
9
Principio di sostituzione di Liskov
Gli oggetti della sottoclasse devono rispettare il contratto della
sovraclasse il contratto puo essere esteso per coprire ulteriori casi.
Questo garantisce che moduli che usano oggetti di un tipo devono potere
usare oggetti di un tipo derivato senza accorgersi della differenza
10
5
04/06/2014
Es: Principio di Sostituzione OK
L estensione pura MaxIntSet soddisfa il contratto di IntSet:
ha tutti i metodi di IntSet, ciascuno con la stessa specifica che in IntSet
ha in più il metodo max, ma utilizzatore di IntSet comunque non lo userà!
Es. IntSet ha metodo iterator():
//@ensures (*restituisce un iteratore su tutti e soli gli elementi di
//@ this, ciascuno visitato una sola volta, in ordine qualunque *);
public Iterator<Integer> iterator()
Codice che usa IntSet e iterator():
}
public static int traccia(IntSet x) {
int somma=0;
(for Iterator<Integer> i: x)
somma+=i.next();
return somma;
Poiché MaxIntSet ha ancora il metodo iterator() con la stessa specifica, il
codice di traccia
sarà sorpreso se gli viene passato un MaxIntSet al
posto di un IntSet: il MaxIntSet si comporta esattamente allo stesso modo.
Quindi traccia(..) continua a garantire il proprio contratto
11
Es: Principio di Sostituzione OK
public static int traccia(IntSet x) {
int somma=0;
(for Iterator<Integer> i: x)
somma+=i.next();
return somma;}
Sottoclasse SortedIntSet ridefinisce la specifica del metodo iterator() (quindi è
estensione non pura):
public class SortedIntSet extends IntSet {
@Override
//@ ensures (* \result contiene tutti e soli gli elementi di this ,
ciascuno una sola volta, in ordine crescente *);
public Iterator<Integer> iterator()
}
traccia(s ); non sarà sorpreso se s è un SortedIntSet: il metodo restituisce comunque
tutti e soli gli elementi, anche se in un ordine particolare
12
6
04/06/2014
Es: Principio di Sostituzione KO!
Se invece iterator() fosse:
//@ ensures (* restituisce un iteratore che itera su tutti gli elementi
positivi di this, ciascuno una sola volta, in ordine crescente *);
public Iterator<Integer> iterator()
}
La traccia(s) non calcola più la traccia dell insieme! il metodo
non è compatibile con quello di IntSet() non restituisce gli
elementi di valore negativo.
Traccia(s) può avere un comportamento scorretto!
Non soddisfa più il proprio contratto.
Il motivo è che il contratto di iterator() in SortedIntSet non
mantiene la promessa fatta dal contratto di iterator() in IntSet.
13
Regole per la specifica di sottoclassi
Come garantire che il contratto dell estensione sia compatibile
con quello della superclasse?
Principio di sostituzione impone vincolo sulla specifica del sottotipo:
deve essere compatibile con specifica del sopratipo (equivalenza
comportamentale (behavioral) tra esemplari della sovraclasse e della
sottoclasse).
Poi basta che implementazione sia corretta rispetto a specifica
Basta mostrare le seguenti tre proprietà della specifica dei tipi
per compatibilità:
Regola della segnatura: un sottotipo deve avere tutti i metodi del
sopratipo, e segnature dei metodi del sottotipo devono essere
compatibili.
Regola dei metodi: le chiamate ai metodi del sottotipo devono
comportarsi come le chiamate ai metodi corrispondenti del sopratipo.
Regola delle proprietà: sottotipo deve preservare tutti i public invariant
degli oggetti del sovratipo.
14
7
04/06/2014
Spiegazione
Regola della segnatura: garantisce che il contratto della
sovraclasse sia ancora applicabile, ossia che la sintassi della
sottoclasse sia compatibiile con la sintassi della sovraclasse
Es. il metodo non cambia la segnatura
Regola dei metodi: verifica che il contratto dei singoli metodi
ereditati sia compabile con il contratto dei metodi originali
Es. estensione pura non cambia specifica
Regola delle proprietà: verifica che la specifica nel suo
complesso sia compatibile con quella originale
15
Regola della segnatura
Garantisce type-safety, ossia che
ogni chiamata corretta (senza errori di tipo) per il sovratipo sia corretta
anche per il sottotipo
correttezza verificabile staticamente
Es.
chiama il metodo iterator(): questo deve essere
presente nell estensione, con un prototipo utilizzabile da
In Java (nelle versioni <1.5), la regola delle segnatura diventa:
un sottotipo deve avere tutti i metodi del sovratipo, e le segnature dei
metodi del sottotipo devono essere identiche alle corrispondenti del
sovratipo
però un metodo del sottotipo può avere meno eccezioni nella
segnatura (il codice che fa uso dell astrazione, scritto con
riferimento al metodo del sovratipo, funziona anche se alcune delle
eccezioni non vengono lanciate dai metodi del sottotipo)
In realtà la regola della segnatura in Java è inutilmente
restrittiva...
16
8
04/06/2014
Esempio: Punti e Linee Colorate
public class Line
public class ColoredLine extends Line {//una Line con un colore
public class Point
un punto (immutabile) nello spazio 2D
public class GridPoint extends
che deve stare su una griglia:
//un GridPoint ha coordinate x e y intere
public Line newLine(GridPoint p)// \result e una linea da this a p
}
public class ColoredGridPoint extends GridPoint {
private Colore col;
// \result è una ColoredLine colorata come this.col
@Override
public Line newLine(GridPoint p)
}
In Java la definizione di newLine è corretta, anche se a run time
restituisce una ColoredLine, che è sottotipo di Line.
Invarianza del risultato e dei parametri
public static void usaPunto(GridPoint punto1) {
Line lin= punto1.newLine(new GridPoint
}
usaPunto(new ColoredGridPoint
La chiamata è lecita in Java perché ColoredGridPoint è sottotipo di
GridPoint.
Ridefinizione di newLine ha la stessa signature delloriginale, ossia:
@Override // result è una ColoredLine colorata come this.col
public Line newLine(GridPoint p)
Allora usaPunto(new ColoredGridPoint
invoca la nuova
newLine, che riceve in ingresso un GridPoint e restituisce una
ColoredLine
Sappiamo che e corretto in Java! ColoredLine è sottotipo di Line e
quindi lin a run-time può riferire un oggetto di tipo ColoredLine.
9
04/06/2014
Covarianza del risultato
public static void usaPunto(GridPoint punto1) {
}
Se fosse consentito ridefinire newLine come:
@Override // \result è una ColoredLine colorata come this
public ColoredLine newLine(GridPoint p)
allora
invocherebbela la nuova
newLine, che riceve in ingresso un GridPoint e restituisce una ColoredLine
E corretto! ColoredLine è sottotipo di Line e quindi lin a run-time può
riferire un oggetto di tipo ColoredLine.
In effetti Java (da 1.5 in poi) consente di restringere il tipo del valore
ritornato (ossia consente la Covarianza del Risultato)
Covarianza dei parametri???
public static void usaPunto(GridPoint punto1) {
}
Se fosse consentito ridefinire newLine come:
@Override // \result è una linea colorata come p.col
public Line newLine(ColoredGridPoint p)
allora
invocherebbe la la nuova
newLine, che deve ricevere in ingresso un ColoredGridPoint
SCORRETTO! Il codice esistente di usaPunto passa a newLine un
GridPoint (che non ha il colore!): errore di tipo a run-time.
Quindi non si può restringere il tipo del parametro GridPoint ad un
sottotipo ColoredGridPoint. Non vale covarianza dei parametri.
10
04/06/2014
Controvarianza dei parametri
public static void usaPunto(GridPoint punto1) {
Line lin= punto1.newLine(new GridPoint
}
usaPunto(new ColoredGridPoint
Se fosse consentito ridefinire newLine come:
@Override // \result è una linea colorata come this.col
public Line newLine(Point p)
allora usaPunto(new ColoredGridPoint
deve ricevere in ingresso un Point
invocherebbe la la nuova newLine, che
CORRETTO! Il codice esistente di usaPunto passa a NewLine un GridPoint, che è
sottotipo di Point.
Quindi si può «allargare» il tipo dei parametri a una sovraclasse (si chiama
Controvarianza dei parametri).
ATTENZIONE: Questo è type-safe ma NON è consentito in Java!!!!!
DOMANDA: perché Java, definito originalmente con invarianza dei parametri e dei risultati, a un
certo punto ha consentito Covarianza dei risultati, ma ancora non consente Controvarianza dei
parametri, pur se type-safe?
Definizioni formali di covarianza e
controvarianza
Una trasformazione di tipo P e' un mapping da tipi a tipi.
Es. costrutto array associa un tipo T a un tipo array_of_T
P e' COVARIANTE se per tutti i tipi T,S quando S è sottotipo di T
allora P(S) e' sottotipo di P(T)
ossia mantiene l'ordinamento dei tipi indotto dalla relazione sottotipo
P e' CONTROVARIANTE se per tutti i tipi T,S quando S è sottotipo
di T allora P(T) e' sottotipo di P(S)
ossia inverte l'ordinamento.
P e' detta invariante negli altri casi (es. misti, ecc.)
NB: terminologia deriva da trasformazione delle coordinate negli
spazi vettoriali
enti covarianti (es. la base ortonormale, per una rotazione degli assi; il gradiente
di un campo scalare, per un cambio di scala): seguono una trasformazione uguale
a quella delle coordinate;
enti controvarianti (es. un vettore): seguono la trasformazione opposta.
25
11
04/06/2014
Regola dei metodi
le chiamate ai metodi del sottotipo devono comportarsi come le chiamate
ai metodi corrispondenti del sopratipo
Non può essere verificata dal compilatore
Perché la chiamata a un metodo del sottotipo abbia lo stesso effetto, basta
che la specifica sia la stessa (e quindi ok con estensioni pure):
se y ha tipo statico IntSet, dopo y.insert(x), sappiamo che x è nell insieme y
quando la chiamata termina (indipendentemente dal tipo effettivo di y, se un
IntSet o un MaxIntSet).
se p ha tipo statico Poly e p.coeff(3) restituisce un valore >0, sappiamo che il
grado di p è almeno 3 (indipendentemente dal tipo effettivo di p).
Ma spesso è necessario cambiare la specifica!
Es. iterator() in SortedIntSet() non restituisce gli elementi in un ordine qualsiasi
ma in ordine crescente
In questo caso, è corretto farlo, perche la ensures di IntSet.iterator() era
nondeterministica: qualunque ordine in cui si ritornano gli elementi andava
bene. Allora ritornarli in ordine crescente è accettabile ( rafforziamo la
postcondizione ).
Valgono regole della precondizione più debole e della postcondizione più
forte
26
Sulla Forza e Debolezza delle Condizioni (1)
Che significano?
FORTE: più restrittivo, meno facile da rendere vero, verificato in meno casi
DEBOLE: meno restrittivo, più facile da rendere vero, verificato in più casi
Es: x > 15 è più forte di x > 7, detto altrimenti {x | x > 15} {x | x > 7})
Come si formalizza in Logica Matematica la forza di una condizione?
le condizioni (formule logiche) sono ordinate (anche se non totalmente): dalle più
forti (vere in meno casi) alle più deboli (vere in più casi)
a un estremo FALSE, la condizione più forte di tutte
all altro estremo TRUE, la più debole che ci sia
l operatore logico per indicare che è più forte di è l implicazione ==>
l implicazione logica è una specie di operatore di relazione
che confronta il
valore di verità delle formule
l implicazione corrisponde all inclusione insiemistica dei valori che rendono
vere le formule (dei casi in cui la formula è vera, o modelli)
Es: se è x>15, è x>7, vale l implicazione ==>
in termini insiemistici {x | x > 15} {x | x > 7}
27
12
04/06/2014
Sulla Forza e Debolezza delle Condizioni (2)
Effetto degli operatori logici sulla forza delle condizioni
Disgiunzione (OR, ||) indebolisce
rispetto alla formula , la formula
in cui è vera
||
è vera in qualche caso in più: quelli
Es. (1<x<10) è più forte di (1<x<10) || (20<x<30)
Congiunzione (AND, &&) rafforza
rispetto alla formula , la formula &&
quelli in cui è vera ma non è vera
è vera in qualche caso in meno:
Es. (1<x<10) è più debole di (1<x<10) && dispari(x)
soddisfatte rispettivamente da [2 .. 9] e da {3, 5, 7, 9}
Implicazione (passare da ad ==> ) indebolisce
rispetto alla formula , la formula ==> è vera in qualche caso in più:
quelli in cui è falsa (infatti ==> equivale a ! || )
Es. (1<x<10) è più forte di dispari(x) ==> (1<x<10)
soddisfatte rispettivamente da [2 .. 9] e da [2 .. 9] {x | pari(x)}
inoltre un implicazione si indebolisce se viene rafforzata la premessa
28
Precondizione più debole
Se la precondizione del metodo ridefinito è più debole di quella
del metodo originale, allora tutti i casi in cui si chiamava il
metodo originale si può chiamare anche il metodo ridefinito.
Precondizione: ciò che chiamante deve garantire al chiamato
perché un metodo operi correttamente
se specifichiamo un metodo indebolendo la precondizione, il
chiamante la verifica a fortiori
Regola della precondizione: presuper => presub
In JML questo è sempre verificato
29
13
04/06/2014
Se la precondizione fosse più forte?
public class Stack<T> {
//OVERVIEW: una pila di elementi di tipo T
//..
//@requires true;
//@ensures (* inserisce v in cima a this *);
public void push(T v)
}
public class BoundedStack<T> {
//OVERVIEW: una pila di elementi di tipo T
// di dim. max pari a cento
...
//@requires this.size() <=100;
//@ensures (* inserisce v in cima alla pila *);
public void push(T v)
}
Non c è modo di specificare BoundedStack come erede di Stack.
Se BoundedStack estendesse Stack, allora codice che usa Stack potrebbe non
funzionare
Es. il metodo statico:
//@ensures (* inserisce 200 elementi in s*)
public static void riempiStack (Stack s) {}
riempiStack funzionerebbe con uno Stack, ma non con un BoundedStack,
violando il princ. di sostituzione.
Ovviamente Java consente di definire BoundedStack come erede di
Stack...pero la sua implementazione violera la specifica!
30
Postcondizione più forti
Postcondizione:
ciò che il chiamato deve garantire al chiamante al termine
dell esecuzione, se vale precondizione
Se rafforziamo postcondizione, allora la postcondizione attesa
dal chiamante sarà comunque verificata
più forte nel senso di implica logicamente :
postsub ==> postsuper
(se postsub è vera, allora anche postsuper è vera)
poiché al termine dell esecuzione del metodo, post sub deve valere,
anche postsuper vale, e l utilizzatore del sopratipo non è sorpreso
In JML questo è sempre verificato
31
14
04/06/2014
Esempio dal calcolo numerico
public class Num {
//requires r > 0
//ensures abs(\result * \result - r) < 0.1
}
public class NumPreciso {
//requires r > 0
///ensures abs(\result * \result - r) < 0.01
}
NumPreciso può essere definita come erede di Num: la sua post garantisce la
post originaria
32
Esempio di violazione della regola dei metodi
public class CharBuffer {
//OVERVIEW: Un buffer di caratteri.
public class LowerCaseCharBuffer {
//OVERVIEW: Un buffer di caratteri minuscoli.
...
}
// se x e minuscolo inserisce x in this, se non
e
// minuscolo non assicura nulla
}
Se LowerCaseCharBuffer venisse definito come sottoclasse di
CharBuffer, il principio di sostituzione verrebbe violato.
La regola della segnatura è verificata, ma la regola dei metodi
NO:
La post di insert non inserisce caratteri minuscoli: è più debole.
33
15
04/06/2014
JML ed estensioni
Come si ridefinisce in JML la specifica di un metodo?
Una sottoclasse eredita pre e postcondizioni dei metodi pubblici e protetti della
superclasse e i sui invarianti pubblici
Sintatticamente: tutto come al solito, basta aggiungere //@also
//@also
Ci dice che la specifica non è completa,
ma serve quanto definito nella superclasse
Vanno considerate insieme a
quanto definito nella superclasse
Semanticamente: clausole aggiuntive interpretate in modo da rispettare la
regola dei metodi
la nuova postcondizione si applica solo nel caso in cui valga la nuova
precondizione
In JML è impossibile specificare sottoclassi che non siano sottotipi perchè
non seguono la regola dei metodi
e perciò tutti i nostri (contro)esempi di violazione della regola dei metodi non
sarebbero accettati da JML
34
Semantica in JML
la parte //@requires della classe erede va in OR (||, disgiunzione)
con quella della classe antenato: requires risulta indebolita
la parte //@ensures della classe erede è essenzialmente messa in
AND con quella della classe antenato: ensures risulta rafforzata
Specifica Superclasse
Requires Presup
Ensures Postsup
Specifica Sottoclasse: //@also
Requires Presotto
Ensures Postsotto
Requires Presup || Presotto
Ensures (\old(Presup ) ==> Postsup)) && (\old(Presotto) ==> Postsotto )
35
16
04/06/2014
Esempio (1)
Contratto di un metodo della classe Baratto: se mi dai almeno dieci patate allora ti
do almeno due fragole
int fragole(int patate)
//@requires patate>=10
//@ensures \result >= 2
Esempio di ridefinizione del metodo in una estensione di Baratto:
tutto come prima, ma inoltre se mi dai almeno cinque patate ti do
fragola
//@also
//@requires patate >=5
//@ensures \result>=1
almeno una
La ridefinizione ha la seguente specifica:
//@requires patate>=10 || patate >=5
//@ensures (patate>=10 ==> \result >= 2) &&
(patate>=5 ==> \result >=1)
se mi dai almeno dieci patate ti do almeno due fragole, se mi dai almeno cinque
36
patate ti do almeno una fragola
Esempio (2)
Se volessi ridefinire fragole indebolendo la postcondizione, cioe dicendo
che voglio restuire meno fragole?
//@also
//@requires patate >=10
//@ensures \result>=1
La ridefinizione ha la seguente specifica:
//@requires patate>=10 || patate >=10
//@ensures (patate>=10 ==> \result >= 2) &&
(patate>=10 ==> \result >=1)
cioe :
cioe :
//@requires patate>=10
//@ensures (patate>=10 ==> \result >= 2)
Infatti non e possibile indebolire la postcondizione in JML.
37
17
04/06/2014
Esempio (3)
Se volessi ridefinire fragole rafforzando la postcondizione, cioe dicendo
che voglio restituire più fragole?
//@also
//@requires patate >=10
//@ensures \result>=4
La ridefinizione ha la seguente specifica:
//@requires patate>=10 || patate >=10
//@ensures (patate>=10 ==> \result >= 2) &&
(patate>=10 ==> \result >=4)
cioè:
//@requires patate>=10
//@ensures (patate>=10 ==> \result >= 4)
Quindi per rafforzare la postcondizione, a parita di precondizione, basta
ripetere la precondizione originale e aggiungere la nuova postcondizione
38
piu forte.
Regola completa della postcondizione
Dagli esempi si vede come, dove non vale presuper, può valere
una postsub diversa o incompatibile con postsuper.
(presuper && postsub) => postsuper
La regola della postcondizione più forte vale quindo solo
dove è verificata la precondizione originale:
il codice che usa il metodo della superclasse non chiama il metodo nei
casi aggiunti dalla precondizione più debole nella versione della
sottoclasse
La regola completa della postcondizione è sempre verificata in
JML, per il modo in cui sono unite le specifiche del metodo
nella superclasse e nella sottoclasse.
39
18
04/06/2014
Esempio di Regola completa post.
Esempio: metodo addZero() di IntSet aggiunge 0 solo negli insiemi
non vuoti
//@requires this.size() > 0
public void addZero()
Definiamo sottotipo di IntSet in cui AddZero() ridefinito in modo che
se l insieme è vuoto viene aggiunto 1
//@also
//@requires this.size() = 0
//@ensures this.isIn(1)
public void addZero()
ensures è diversa solo per quei valori (this = vuoto) che non erano legali
per addZero() della superclasse: il codice che usa addZero non è sorpreso
dalla modifica (non chiamera mai addZero con this == vuoto)
In JML, la postcondizione corrisponde a:
(\old(size()>0) ==> isIn(0) ) && (\old(size()=0) ==> isIn(1) )
40
Esempio con tipi primitivi
int (Integer) è sottotipo di long (Long)? O viceversa
Osservazione:
la somma di due int a 32 bit in caso di overflow lancia eccezione,
mentre la somma degli stessi numeri rappresentati come long a 64 bit
calcola il risultato!
Non possono essere uno sottotipo dell altro perche le
rispettive postcondizioni della somma non si implicano.
41
19
04/06/2014
Riassumendo
1. Regola dei metodi può essere enunciata come:
require no more, promise no less:
NON RICHIEDERE DI PIU' del metodo della classe base
NON PROMETTERE DI MENO del metodo della classe base
Entrambe le richieste devono essere soddisfatte
JML impedisce di specificare astrazioni sui dati che violino
la regola dei metodi
NB: Ci sono altri metodi di specifica che lo consentono
in JML, al massimo si può costruire una specifica non soddisfacibile
(pre e/o post condizioni sono false per tutti i valori)
Tuttavia, una classe in Java può essere implementata in modo
scorretto e violare la regola.
42
Attenzione quando si eliminano eccezioni!
IntSet con insert che non ignora i duplicati, ma
lancia un eccezione:
sottoclasse elimina eccezione:
public class IntSet extends ExIntSet {...
public class ExIntSet {
//@ensures !\
//@ signals (DuplicateException e) \old(isIn(x));
public void insert (int x) throws DuplicateException
//NON LANCIA ECCEZIONE
public void insert (int x)
}
}
Regola della segnatura: OK, ma Regola dei metodi: KO!
Utilizzatore di IntSet potrebbe usare l eccezione Duplicate anche per stabilire se
l elemento era gia presente e sara sorpreso...
Dim: Sia x in this. Postsub è vera. Ma PostSuper è falsa (eccezione non è lanciata).
Quindi si può eliminare un eccezione dalla segnatura solo se non è effettivamente
usata o se il suo lancio è opzionale
Ad esempio se era prevista non per trattare violazioni di precondizioni sui dati, ma per il verificarsi di
altre condizioni che non possono più verificarsi. Notare la differenza con le precondizioni, che
possono invece essere indebolite.
Es. SportelloApertoException usata per metodo read() di una classe che descrive un floppy e poi
in una sottoclasse che descrive una memoria SD rimovibile.
43
20
04/06/2014
Es. eliminazione eccezioni
Nell es. BoundedStack non può essere definita come erede di Stack.
La Stack può essere definita come erede di BoundedStack?
Stack.push: //@ ensures (* inserisce v in cima *);
BoundedStack.push:
//@ requires this.size() <=100;
//@ ensures (* inserisce v in cima *);
SI, la regola dei metodi è soddisfatta.
Se però contratto di BoundedStack.push fosse:
//@ signals (OverflowExcepion e) this.size() >100;
//@ ensures \old(size())<100 ==> (* inserisce v in cima *);
allora violata regola della postcondizione.
44
Regola delle proprietà
Sottotipo deve conservare le proprietà degli oggetti del sovratipo
Sono proprietà generali incluse nel contratto della classe, e deducibili dal
contratto dei metodi. Non compaiono pero esplicitamente nei metodi
proprietà definite tipicamente nella OVERVIEW o come public invariant
del sopratipo.
Occorre mostrare che tutti metodi nuovi o ridefiniti, inclusi i costruttori, del
sottotipo conservano le proprietà invarianti e le proprietà evolutive del
sovratipo, osservabili con i metodi pubblici observer della sopraclasse
Si usa solo specifica dei metodi, non implementazione. Fra un osservazione e
l altra, e possibile che vengano chiamati anche i metodi nuovi dell estensioe.
proprietà invariante: proprietà degli stati astratti osservabili dalla
sopraclasse ().
es: size() di un IntSet è sempre >= 0. Grado di un Poly non è negativo.
proprietà evolutiva: relazione fra uno stato astratto osservabile e lo stato
astratto osservabile successivo
Es. Mutabilità; grado di un Poly non cambia
45
21
04/06/2014
Esempio violazione proprietà invariante
tipo FatSet: come IntSet ma non è mai vuoto:
public class FatSet {
//OVERVIEW Un SimpleSet è insieme mutabile di interi con
// almeno un elemento
//@ public invariant this.size()>=1; //sempre almeno un elemento
//@ ensures (*costruisce insieme {i}*)
public FatSet(int i)
//@ ensures \old(this.size()>=2) ==> !this.isIn(x); //elimina x da this
public void removeNonEmpty(int x)
}
public class IntSet {
...
//@ensures !this.isIn(x);
}
IntSet non può essere definita come sottoclasse di FatSet (IntSet extends FatSet)
perché ne viola la proprietà (anche solo aggiungendo costruttore IntSet() per
l insieme vuoto). Notare che IntSet sembra estensioen pura di SimpleSet (ma non
lo e perche ne viola le proprieta )
46
Esempio violazione proprietà evolutiva
Tipo SimpleSet come IntSet ma senza remove:
public class SimpleSet
//OVERVIEW Un SimpleSet è insieme mutabile di
// interi che non può ridursi nel tempo
IntSet non può essere definito come estensione pura di
SimpleSet aggiungendo remove, perché ne viola proprietà
Utilizzatori di SimpleSet sarebbero sorpresi non ritrovando più gli
elementi che avevano inserito in precedenza in un SimpleSet!
47
22
04/06/2014
Altro esempio di violazione proprietà
evolutiva
Sottoclasse di Stack che aggiunge un metodo riflesso
public class MirrorStack extends Stack {
//@ensures (*this diventa il riflesso di \old(this) *);
}
Pur essendo un'estensione pura di Stack, viola la proprietà
evolutiva delle Pile (ossia la politica LIFO)
Codice utilizzatore sarebbe sorpreso di non trovare i dati in
ordine LIFO.
NB: Quindi anche un'estensione pura può violare il principio di
sostituzione
Spesso si preferisce allora definire le estensioni pure come quelle che non
modificano la specifica dei metodi e mantengono le proprietà della
classe.
48
Ereditarietà e collezioni
class Automobile {...}
class AutomobileElettrica extends Automobile {...}
class ParcheggioAutomobili {
public void aggiungi(Automobile a) {
//@ensures (*inserisce auto a in parcheggio*)
....
}
La classe ParcheggioElettriche rappresenta parcheggi speciali dedicati
esclusivamente alle AutomobiliElettriche.
ParcheggioElettriche può essere sottotipo di ParcheggioAutomobili?
public class ParcheggioElettriche extends Parcheggio {
}
50
23
04/06/2014
Parcheggio
Automobile a=new Automobile();
Parcheggio_di_Automobili p=new ParcheggioElettriche(100);
p.aggiungi(a);
Sorpresa: inserisce Automobile non elettrica in Parcheggio_di_Elettriche
(violata regola delle proprietà)!
Se per impedirlo si ridefinisse ParcheggioElettriche.aggiungi(Automobile) in
modo da inserire solo Auto elettriche, si violerebbe invece la postcondizione di
Parcheggio.aggiungi(Automobile)!
quindi un ParcheggioElettriche non può essere definito come sottotipo di
ParcheggioAutomobili
Questo perche' ParcheggioAutomobili e' un tipo Mutabile. Se fosse immutabile,
non ci sarebbe metodo aggiungi(): un ParcheggioElettriche potrebbe essere
definito come estensione di ParcheggioAutomobili (il costruttore non e'
ereditato...)
E' lo stesso problema già visto con i generici: Collection<String> non e'
sottotipo di Collection<Object>
51
Riassumendo: il principio di sostituzione
Tre proprietà della specifica dei tipi per compatibilità:
Regola della segnatura: un sottotipo deve avere tutti i metodi del
sopratipo, e segnature dei metodi del sottotipo devono essere
compatibili.
Garantito dal compilatore Java
Regola dei metodi: le chiamate ai metodi del sottotipo devono
comportarsi come le chiamate ai metodi corrispondenti del sopratipo.
Garantito da JML ma non da Java
Regola delle proprietà: sottotipo deve preservare tutti i public invariant
e le proprieta evolutive degli oggetti del sovratipo.
Garantito in parte da JML
L implementazione Java deve essere aderente alla propria
specifica.
52
24
04/06/2014
Consigli per usare ereditarietà
Un approccio errato
Ereditarietà = riuso diretto codice.
Es: classe Persona eredita da classe Data perché ha una data di
nascita
Approccio corretto: principio di sostituzione
Un oggetto della classe derivata deve potere essere sostituito
ovunque ci sia un oggetto della classe base.
Persona non può essere usato dove c'è una Data! Vi siete iscritti in
data "Mario Rossi"?
Ereditarietà quindi non è un meccanismo di condivisione/riuso del
codice: la sottoclasse deve essere simile alla sopraclasse
53
Esempio: Quadrato vs Rettangolo
Un Quadrato può essere erede di Rettangolo?
(es: costruttore public Quadrato(float l){ lato1 = lato2 = l})
Dipende (di solito no): Se Rettangolo ha metodo stretch() per allungare o
public void stretch() //@ensures (*cambia rapporto tra i lati*)
Tipica soluzione corretta:
classe astratta Figura, e poi Rettangolo e Quadrato definiti come eredi di
Figura. Se si vuole riusare in Quadrato il codice scritto per Rettangolo
basta p.es. che Quadrato includa un attributo privato di tipo Rettangolo.
54
25