Estensioni
Estensioni pure
• 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
2
Estensione pura MaxIntSet: Specifica
• Come IntSet, ma ha metodo per estrarre il massimo elemento.
Quindi specifica di tutti gli altri metodi è inalterata.
public class MaxIntSet extends IntSet {
// OVERVIEW: MaxIntSet è sottotipo di IntSet con metodo max per
//estrarre il massimo elemento
//costruttori:
public MaxIntSet(){
//@ensures (*inizializza this come il MaxIntSet vuoto*)
}
//metodi:
public int /* pure */ max() throws EmptyException {
//@ ensures \result>= (\max int i; this.isIn(i);i);
//@signals(EmptyException) this.size() == 0;
}
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! (insert e remove)—di
fatto, cambia RI.
public class MaxIntSet extends IntSet {
private int biggest;//memorizza il max. Non definito per this=vuoto.
public MaxIntSet(){ super(); }
public void insert(int x){
overriding
if (size() == 0 || x>biggest) biggest = x;
super.insert(x); //chiama metodo insert di IntSet
}
public void remove(int x){
super.remove(x);
if(size()==0||x<biggest) return;
Iterator g=elements();
biggest=((Integer) g.next()).intValue();
while(g.hasNext() {
int z=((Integer) g.next()).intValue();
if(z>biggest) biggest=z;}
public int max() throws EmptyException {
if (size() == 0) throw new EmptyException(“MaxIntSet.max);
return biggest;}
}
ridondante
(ridefinizione)
4
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)
• Il rep invariant della sottoclasse non ha bisogno di riportare il rep invariant della sovraclasse
(perché questo è comunque ereditato senza possibilità di modifca. In JML si scrive “also” per
dire che il nuovo RI viene “aggiunto” a quello ereditato.
// il rep invariant RI_MaxIntSet(c) è:
//@ also
//@ private invariant this.size>0 ==>
//@
(this.isIn(this.biggest) &&
//@
(\forall int x; this.isIn(x); x <= this.biggest));
RI è quindi sempre vero quando this è l’insieme è vuoto. In tal caso, biggest può assumere un
valore qualunque.
NB: Se serve, si possono usare parti pubbliche della sovraclasse per definire RI. Infatti le parti
private della superclasse non si possono utilizzare nell’invariante. Quindi RI di una
sottoclasse può usare: gli attributi privati della classe, gli attributi protected ereditati, i metodi
puri pubblici ereditati
Es. solo se els fosse protected si potrebbe scrivere al posto dell’ultima riga:
(\forall int i; 0<= i && i<this.size(); els.get(i) <= this.biggest)
5
Un caso particolare di estensioni pure:
implementazioni multiple
Quando usare classi astratte e interfacce?
Attributi protected
Poly densi e sparsi
• DensePoly: una implementazione di Poly adatta al caso in cui ci sono pochi coefficienti nulli
(ad es. quella vista per i Poly con un array per tutti i coefficienti);
• SparsePoly: un’altra implementazione che è efficiente quando molti coefficienti sono nulli
(es. lista a puntatori, in cui ogni nodo memorizza il coeff. e il grado di ogni termine!=0).
• Se usiamo questa soluzione:
DensePoly
SparsePoly
• In DensePoly il rep include un array! Questo è ereditato da SparsePoly! Potremmo ignorarlo e
dichiarare comunque una lista, ma l’instance variable terms sarebbe comunque presente:
– Occupa memoria inutile.
– potremmo dimenticare di ridefinire qualche operazione che usa il rep dei DensePoly (non ce ne
possiamo accorgere a compile time!)
7
Implementazioni multiple
• Soluzione: definire una classe Poly in modo che non memorizzi elementi:
saranno sottoclassi a stabilire modalità di memorizzazione
• Poly deve diventare astratta: non è possibile fare add, ecc. senza il rep
Gerarchia di tipi può essere utilizzata per fornire più implementazioni dello
stesso tipo
– DensePoly e SparsePoly possono essere definiti come sottotipi di Poly.
Poly
DensePoly
SparsePoly
• Il tipo da implementare è di solito descritto con interfaccia (se nessuna
operazione è implementabile) o classe astratta (se alcune operazioni sono
implementabili)
8
Il tipo Poly
public abstract class Poly {
//@ ensures (* \result == grado del polinomio *);
public abstract int degree(){}
//@ ensures (* \result == coeff. del termine di grado d *);
public abstract int coeff(int d){}
//@ ensures (* \result == this + q *);
//@ signals (NullPointerException e) q == null;
public abstract Poly add(Poly q) throws NullPointerException {}
//@ ensures (* \result == this - q *);
//@ signals (NullPointerException e) q == null;
public abstract Poly sub(Poly q) throws NullPointerException {}
//@ ensures (* \result == this * q *);
//@ signals (NullPointerException e) q == null;
public abstract Poly mul(Poly q) throws NullPointerException {}
//@ ensures (* \result == -this *);
//@ signals (NullPointerException e) q == null;
public abstract Poly minus() {}
//@ ensures (* \result == iteratore su tutti gli elementi di this in ordine dal coeff di grado 0 al coeff di
grado degree() *);
public Iterator terms() {}
Utilizzatore di Poly “vede” solo i metodi definiti in Poly.
//@ ensures (* \result == derivata di p *);
public static Poly derivata(Poly p)
Non importa se p sarà un DensePoly o uno SparsePoly.
9
Protected
• La Poly potrebbe definire almeno una parte del rep, che dia il
grado del polinomio. Questa è un’informazione che deve
essere presente in tutte le implementazioni di Poly.
– In questo modo si può implementare anche la degree().
• Se è private, non è usabile nelle sottoclassi, se è public espone
il rep. Esiste un altro modificatore:
protected = visibile alle sottoclassi (e a classi nello stesso
package)
public abstract class Poly {
protected int deg;
//@ ensures (* \result == grado del polinomio *);
public int degree(){return deg;}
10
Riassunto Accesso ed ereditarietà
•
Attributi e metodi di una classe possono essere:
– public
• sono visibili a tutti
• vengono ereditati
– private
• sono visibili solo all’interno della stessa classe
• non sono visibili nelle sottoclassi, ma sono ereditati
– protected
• sono visibili solo alle sottoclassi e alle classi nello stesso package
• vengono ereditati
– “friendly”:
• sono visibili a tutte le classi nello stesso package
• vengono ereditati, ma sono visibili alle sottoclassi che stanno nella
stesso package della classe
11
Quando usare protected?
• Membri protected dovrebbero essere evitati se non necessari:
– senza di loro classe può essere reimplementata senza disturbare l’
implem. delle sottoclassi
– sono visibili nello stesso package, e quindi altro codice potrebbe
interferire con la loro implementazione
• Si introducono per consentire implementazioni efficienti per le
sottoclassi
– Primo modo: protected instance variables
– Secondo modo (da preferire): private instance variables ma accesso
tramite metodi protected. Utile per
• consentire a sovraclasse di mantenere invariante
• mantenersi la possibilità di cambiare il rep, ridefinendo
opportunamente i metodi protected
12
Implementazione parziale di Poly
• Il campo deg è presente in tutti i Poly: perche’ non inizializzarlo in Poly?
Inizializzazione va fatta dai costruttori e la classe Poly è abstract!
• Ma si può comunque definire un costruttore!
public abstract class Poly {
protected int deg;
//costruttori
//@ ensures (* inizializza this a grado n *);
protected Poly(int n){}
//è protected perché non ha senso definire il Poly di grado n: serve solo per
//inizializzare un pezzo del rep. Se fosse public, le sottoclassi di Poly dovrebbero
//ridefinirlo. Cosi’ lo chiamano con super(n);
//@ ensures (* \result == grado del polinomio *);
public int degree(){return deg;}
…//qui tutti gli altri metodi di Poly, astratti
}
13
Implementazione con DensePoly
public class DensePoly extends Poly{
private int[] trms; //array per memorizzare i coeff.
//costruttori
//@ ensures this.degree() == 0 && this.coeff.(0)==0 ;
public DensePoly(){
super (0); trms=new int[1];}
public DensePoly(int c, int n) throws NegativeExponentException {...}
public poly add(Poly q) { //implementa la abstract add di Poly
if (q instanceof SparsePoly) {...}
//la def. di add tra un DensePoly e uno SparsePoly è ad hoc
else {...} //codifica di add di due DensePoly
...
}
• La SparsePoly è analoga ma usa una lista...
14
Combinare Densi e Sparsi
• polinomi sono dichiarati tutti di tipo Poly: poi si chiama il costruttore di
DensePoly o di SparsePoly a seconda dellla definizione preferita.
Poly p1 = new DensePoly();
Poly p2 = new SparsePoly();
….//qui inseriamo monomi in p1 e p2
Poly p3 = p1.add(p2);
La add è definita come Poly add(Poly)!
• La add di due Poly può essere un DensePoly o uno SparsePoly
– ad es. sommando due SparsePoly si potrebbe ottenere un polinomio con pochi
zeri intermedi: sarebbe più efficiente rappresentarlo con un DensePoly; somma
di un DensePoly e di uno SparsePoly potrebbe a volte essere sparsa, ecc..
• Conviene che add, mult ecc (Produttori) convertano “automaticamente” da
una impl. all’altra, per sfruttare rappresentazione più efficiente!
15
Conversione fra DensePoly e SparsePoly
• Usare un costruttore (“di conversione”):
– Es. in classe SparsePoly mettere costruttore:
//@ ensures (* this come il DensePoly implem. da trms *);
SparsePoly(int []trms)
– il costruttore può essere chiamato da DensePoly per costruire uno SparsePoly
(es. quando la add si accorge che in realtà ci sono molti coeff. nulli...)
– public o protected? public non va bene (utenti potrebbero accedere a rep!),
protected nemmeno (DensePoly non è sottoclasse di SparsePoly)
– usare “friendly”: visibile all’interno dello stesso package
– Però DensePoly e SparsePoly devono essere in stesso package (e
l’implementazione di ciascuna dipende dall’implementazione dell’altra)
– anche un costruttore SparsePoly(DensePoly p) può essere definito per realizzare la
conversione, ma poi può essere poco efficiente (SparsePoly non può accedere a
implementazione di DensePoly...). E’ soluzione migliore dal punto di vista della
manutenzione...
16
Progettare a oggetti
Estensioni con ridefinizione di metodi
Open-Closed Principle
• (dovuto a B. Meyer)
• “Software entities should be open for extension, but closed for
modification”
• "open for extension“ = comportamento dei moduli può essere
modificato per soddisfare cambiamenti nei requisiti
• “closed for modification” = i moduli non possono essere
modificati
• Sembra una contraddizione. Come e’ possibile?
• Il vantaggio in manutenzione è ovvio: se non modifico, non
faccio errori
• Esaminiamo un esempio di progetto tradizionale e progetto a
oggetti per capire che cosa significa...
18
Esempio: Progetto tradizionale in C
typedef struct …Figura;
Figura
Cerchio
Rettangolo
Figura figure[100];
Triangolo
void disegnaTutto(Figura *figure) {
for (i= 0; i<100;i++) {
if (figure[i] è “rettangolo”)
“disegna rettangolo”
if (figure[i] è “triangolo”)
“disegna triangolo”
if (figure[i] è “cerchio”)
“disegna cerchio”
}
}
figure[1] = “rettangolo”;
figure[2] = “triangolo”;
figure[3] = “cerchio”;
Estendere progetto tradizionale: arriva il
Trapezio
Figura
Cerchio
Rettangolo
Triangolo
typedef struct …Figura;
Figura figure[100];
Trapezio
void disegnaTutto(Figura *figure) {
for (i= 0; i<100;i++) {
if (figure[i] è “rettangolo”)
“disegna rettangolo”
if (figure[i] è “triangolo”)
“disegna triangolo”
if (figure[i] è “cerchio”)
“disegna cerchio”
if (figure[i] è “trapezio”)
“disegna trapezio
}}
figure[1] = “rettangolo”;
figure[2] = “triangolo”;
figure[3] = “cerchio”;
figure[4] = “trapezio”
Codice già definito per
disegnaTutto deve cambiare
per potere supportare il
nuovo tipo!!!
Open/closed?
• Quindi progettazione tradizionale non verifica open-closed:
• Il modulo disegnaTutto è aperto a estensioni, ma solo tramite
modifica: non è chiuso rispetto alle modifiche.
• Come si puo’ fare a rispettare open/closed?
21
Es. in versione OO
//si definisce classe astratta Figura, con
metodo astratto disegna(), e sue eredi
Rettangolo, Cerchio, Triangolo che
implementano disegna()
Figura
Figura figure = new Figura[100];
Cerchio
Rettangolo
Triangolo
figure[1] = new Rettangolo();
figure[2] = new Triangolo();
figure[3] = new Cerchio();
…
….disegnaTutto(figure);
public static void disegnaTutto(Figura [] figure) {
for (i= 0; i<100;i++)
figure[i].disegna();
}
Quantità di codice è più o meno la stessa di prima ...
Estendibilità: arriva il Trapezio
Figura figure = new Figura[100];
Figura
Cerchio
Rettangolo
Triangolo
Trapezio
figure[1] = new Rettangolo();
figure[2] = new Triangolo();
figure[3] = new Cerchio();
figure[4] = new Trapezio();
…disegnaTutto(figure);
public static void disegnaTutto(Figura [] figure) {
for (i= 0; i<100;i++)
figure[i].disegna();
}
Codice definito
per Figura non
cambia
Open-closed
• 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() è definita in base alla classe astratta Figura.
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.
24
Estendibile se….
• Estendibilità tramite ereditarietà è garantita solo se possiamo
usare oggetti di una classe che sono “sostituibili” a quelli della
sopraclasse.
• Ad esempio, la disegna() deve contenere codice che disegna
l’oggetto this sullo schermo. Ogni sottoclasse di Figura deve
implementare una disegna() che abbia lo stesso effetto!
• Come fare a garantirlo?
25
Specifica di estensioni
Modificano specifica di sovraclassi
Principio di sostituzione di Liskov
• “gli oggetti di una sottoclasse devono potere essere
sostituiti ovunque siano usati oggetti della sopraclasse,
senza influenzare il comportamento del codice che li usa”
• In altre parole:
• “moduli che usano oggetti di un tipo devono potere usare
oggetti di un tipo derivato senza accorgersi della
differenza”
• Significa che il comportamento della sottoclasse deve
essere “compatibile” con la specifica della sopraclasse
27
Esempio 1
public static int traccia(IntSet x) {
int somma;
for (Iterator i = x.elements(); i.hasNext();)
somma+=((Integer) x.next()).intValue();
return somma;
}
• In una sottoclasse SortedIntSet di IntSet ridefiniamo l’iteratore elements():
public class SortedIntSet extends IntSet {
//@ ensures (* \result == un generatore che produce tutti gli elementi di
//@ this come Integers, ciascuno una sola volta, in ordine crescente *);
public Iterator elements ()
}
• traccia(s ); non sarà “sorpreso” se s è un SortedIntSet: l’iteratore restituisce
comunque tutti gli elementi anche se in un ordine particolare
28
Esempio 2
• Se invece elements() fosse:
//@ ensures (* \result == un generatore che produce tutti gli elementi
//@ dispari di this, come Integers, ciascuno una sola volta *);
public Iterator elements ()
• La traccia(s) non calcola più la traccia dell’insieme! l’iteratore
non è compatibile con quello di IntSet()—non restituisce gli
elementi di valore pari.
• Comportamento scorretto
29
Sottoclassi e sottotipi
• Un tipo S è un sottotipo di un tipo T se S è usabile in ogni contesto
in cui è usabile T.
• Una classe S è una sottoclasse di una classe T se S è dichiarata come
estensione di T: extends T
– La sottoclasse S eredita tutta l’implementazione (attributi e metodi) della
sopraclasse T
• Quindi principio di sostituzione equivale a dire che relazione di
eredtarietà deve essere relazione di sottotipo
• In generale (sotto)classe e (sotto)tipo sono nozioni distinte
– coincidono se viene adottato approccio disciplinato a ereditarieta`
– altrimenti sottoclassi semanticamente svincolate da superclassi; non
rappresentano sottotipi ma tipi diversi costruiti incrementalmente
– Su [Liskov] (sotto)classe e (sotto)tipo usati come sinonimi perche` si
promuove/impone approccio disciplinato
– su [Ghezzi&Jazayeri] (sotto)classe e (sotto)tipo nozioni distinte e si
analizzano condizioni perché coincidano
30
Regole per la specifica di sottotipi
• 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
• 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.
31
Regola della segnatura
• Garantisce che ogni chiamata corretta (senza errori di tipo) per il sovratipo
sia corretta anche per il sottotipo, e ciò deve essere verificabile
staticamente
• In Java, 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...
• (in alcuni linguaggi OO si può violare addirittura regola delle segnature: un
metodo della sovraclasse può essere eliminato nella sottoclasse).
32
Controvarianza e Covarianza (1)
A
f: B → C
Esempio (stilizzato)
Classe A' derivata da classe A
A’
f : B’ → C’
Classe A ha metodo f: B → C
In A' ridefinizione di metodo f : B'
→C'
33
Controvarianza dei parametri
• Perché A’ sia sostituibile ad A (dal punto di vista della tipizzazione delle
chiamate del metodo f) basterebbe che
• Gli argomenti in ingresso di f siano tutti accettabili per f ’, cioè B’sia un
sovratipo di B (controvarianza dei parametri in input)
⇒ una chiamata della f ’ di un esemplare di A’ accetta in ingresso qualsiasi valore
accettato da una qualsiasi chiamata della f su un esemplare di A
Esempio:
public static void usaA(A a0) {
B b0;
...
C c0 = a0.f(b0); ...
}
• Chiamata di f con argomento di tipo B è valida se f prevede un argomento di
tipo B o di un suo sopratipo. Quindi se parametro attuale per a0 fosse di tipo A’,
B’ deve essere di tipo B o di un sopratipo di B (se fosse sottotipo non sarebbe
accettabile)
• TUTTO QUESTO NON SI APPLICA A JAVA!
34
Covarianza dei risultati
C’ sia un sottotipo di C (covarianza sui risultati)
C c0 = a0.f(b0);
⇒qualsiasi valore restituito da una chiamata di f per un esemplare di A’
è accettabile come risultato nel contesto di una chiamata della f su un
esemplare di A, perchè non viene prodotto nulla di “inaspettato”
⇒VALIDO in Java solo da 1.5
B
A.f
B’
C
C
A’.f
B
C’
35
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. elements() in SortedIntSet() non restituisce gli elementi in un ordine
qualsiasi ma in ordine crescente
– In questo caso, è corretto farlo, perche’ la ensures di Set.elements() 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
36
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}
37
Sulla Forza e Debolezza delle Condizioni (2)
• Effetto degli operatori logici sulla forza delle condizioni
– Disgiunzione (OR, ||) indebolisce
• rispetto alla formula α, la formula α || β è vera in qualche caso in più:
quelli in cui è vera β
– Es. (1<x<10) è più forte di (1<x<10) || (20<x<30)
– Congiunzione (AND, &&) rafforza
• rispetto alla formula α, la formula α && β è vera in qualche caso in meno:
quelli in cui è vera α ma non è vera β
– 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
38
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
//@ensures ………
//@requires ………
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 mdo da
rispettare la regola dei metodi
– la parte //@requires della classe erede va in OR (||, disgiunzione) con
quella della classe antenato Î requires risulta indebolita
– la parte //@ensures della classe erede va in AND (&&, congiunzione)
con quella della classe antenato Î ensures risulta rafforzata
39
Quindi
• 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
• Superclasse
– Requires Presup
– Ensures Postsup
Sottoclasse
Requires Presotto
Ensures Postsotto
– Requires Presup || Presotto
– Ensures Postsup && Postsotto
• Usando spesso i commenti (sempre veri in JML), la verifica a
runtime è spesso eccessivamente permissiva e quindi inadeguata
40
Precondizioni più deboli
• Precondizione: ciò che il chiamante deve garantire al chiamato perché un
metodo operi correttamente
• se specifichiamo un metodo indebolendo la precondizione, il chiamante la
verifica a fortiori
– Es. in IntSet ci sia metodo addZero che aggiunge 0 solo se l’insieme non è
vuoto :
//@ requires this.size()>0;
//@ ensures this.isIn(0);
public void addZero()
– e in un sottotipo di IntSet ridefiniamo il metodo:
//@also
//@requires this.size()=0;
public void addZero()
– precondizione è più debole (this.size()>0 || this.size()=0)
– il codice che usava il metodo addZero() non è “sorpreso” dalla nuova
precondizione: non chiama addZero quando this è vuoto. Ma se ora addZero()
funziona con this = vuoto, per il chiamante non cambia nulla
– più debole = “implicato logicamente”
• Regola della precondizione: presuper => presub
41
Se la precondizione fosse più forte?
public class Stack {
//OVERVIEW: una pila di elementi di tipo Object
//@ ensures (* inizializza this alla pila vuota *);
public Stack( )
//@ ensures (* inserisce v in cima a this *);
public void push(Object v)
//@ requires this.size()>0;
//@ ensures (* restituisce ed elimina la cima di this *);
public Object topPop( ) throws EmptyStackException
//@ ensures (* restituisce il numero di elementi di this *);
public int size( )
}
public class BoundedStack {
//OVERVIEW: una pila di elementi di tipo Object di dim. max pari a cento
//@ ensures (* inizializza this alla pila vuota *);
public BoundedStack()
//@ requires this.size() <=100;
//@ ensures (* inserisce v in cima alla pila *);
public void push(Object v)
}
Classe BoundedStack non può essere sottoclasse di Stack. Codice chiamante:
public static void riempiStack (Stack s) { “inserisce 200 elementi in s”}
riempiStack funziona con uno Stack, ma non con un BoundedStack!
42
Postcondizioni 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, postsub deve valere, anche
postsuper vale, e l’utilizzatore del sopratipo non è “sorpreso”
43
Esempio dal calcolo numerico
public class Num {
…
//@requires r > 0
//@ensures abs(\result * \result - r) < 0.1
public float sqrt(float r) {…}
…
}
…
public class NumPreciso {
…
//@also
//@requires r = 0
//@ensures abs(\result * \result - r) < 0.01
…
public float sqrt(float r) {…}
…
}
Nella sottoclasse il radicando può essere anche nullo (presuper => presub)
il risultato deve essere più preciso (postsub => postsuper)
44
Esempio di violazione della regola dei metodi
public class CharBuffer {
//OVERVIEW: Un buffer di caratteri.
…
//@ensures this.isIn(x)
public void insert(char x) {…}
...
}
public class LowerCaseCharBuffer {
//OVERVIEW: Un buffer di caratteri minuscoli.
…
//@ensures minuscolo(x) ==> this.isIn(x)
// se x e’ minuscolo inserisce x in this, se non e’ minuscolo non assicura nulla
public void insert(char x) {…}
…
}
NB: LowerCaseCharBuffer non è sottotipo di CharBuffer, Se venisse definito come
sottoclasse il principio di sostituzione verrebbe violato. La post di insert non inserisce
caratteri maiuscoli e quindi e’ piu’ debole. La regola della segnatura è invece verificata
45
Regola completa della postcondizione
• Come deve essere la postcondizione se la precondizione è indebolita?
– NB: La postcondizione più forte deve valere solo per i casi in cui vale la precondizione
originale, perchè il codice che usa il metodo della superclasse non lo chiama nei casi
aggiunti dalla precondizione più debole nella versione della sottoclasse
– Esempio: metodo addZero() di IntSet aggiunge 0 solo negli insiemi non vuoti
//@requires this.size() > 0
//@ensures this.isIn(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 \old(this.size()>0) ==> this.isIn(0) &&
\old(this.size()=0) ==> this.isIn(1)
public void addZero()
Il metodo ha diffferente ensures 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)
– Regola della postcondizione: (presuper && postsub) => postsuper
– La regola della postcondizione. è verificata
– La regola sarebbe violata se invece postcondizione fosse:
//@ensures this.isIn(1);
46
Riassumendo
• 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
47
attenzione quando si eliminano eccezioni!
• Supponiamo di avere definito in IntSet una insert che non ignora i duplicati, ma lancia
un’eccezione:
public class IntSet {...
//@ ensures !\old(this.isIn(x)) && this.isIn(x);
//@ signals (DuplicateException e) this.isIn(x);
public void insert (int x) throws DuplicateException
}
• Poi sottoclasse (per es. MaxIntSet) elimina eccezione:
public class MaxIntSet extends IntSet {...
//@ also
//@ ensures !\old(this.isIn(x)) ==> this.isIn(x);
public void insert (int x)
}
• Regola della segnatura: OK
• 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 viene lanciata).
• Quindi si può eliminare un’eccezione dalla segnatura solo se non è effettivamente usata o se il
suo lancio e’ 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
(es. SportelloApertoException usata per metodo read() di una classe che descrive un floppy e
poi in una sottoclasse che descrive una memoria SD rimovibile). Notare la differenza con le
precondizioni, che possono invece essere indebolite.
48
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’ la
rispettiva postcondizioni della somma non si implicano.
49
Regola delle proprietà
• “sottotipo deve conservare le proprietà degli oggetti del sovratipo”
– proprietà definite tipicamente 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
• 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
50
Esempio violazione proprietà invariante
• tipo FatSet: come IntSet ma non è mai vuoto:
public class FatSet {
//OVERVIEW Un FatSet è 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);
public void remove (int 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).
51
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 sottoclasse 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!
52
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.
53
Chiarimento su immutabilità e osservabilità
• Se S estende T immutabile, S potrebbe essere mutabile.
• Immutabilità è proprietà evolutiva
– Un sottotipo di un tipo immutabile è pure immutabile, o perlomeno le
sue eventuali mutazioni non sono visibili utilizzando i metodi
osservatori dichiarati nel sopratipo immutabile (in questo modo, il
codice che usava il sopratipo continua a ritenerlo immutabile)
• Quindi l’importante è che, usando solo le operazioni note nella
segnatura di T, il tipo “sembri” immutabile.
• Ad esempio, un erede di Poly potrebbe aggiungere una nuova
componente mutabile dello stato astratto. Questa nuova
componente non è comunque visibile agli utilizzatori di Poly,
che quindi continuano a ritenere Poly immutabile.
54
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
55
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
accorciare una figura…
• public void stretch() //@ensures (*cambia rapporto tra i lati*)
• Quadrato non si può allungare…
56
Esempio: Pinguino vs Uccello
• Un Pinguino può essere erede di Uccello?
– Forse sì, forse no. Però se Uccello ha metodo:
– public void vola(){...} come si fa?
– Se lo togliessimo (impossibile comunque in Java), chi usa
Pinguino pensando che sia un Uccello e quindi abbia vola()
sarà sorpreso spiacevolmente…
– se ridefiniamo metodo che non fa nulla, si sorprende
utilizzatore che si aspetta che post-condizione di "vola" sia
che "quota" sia positiva...
57
Ereditarietà e contenitori
class Automobile {...}
class AutomobileElettrica extends Automobile {...}
class Parcheggio {
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 Parcheggio?
public class ParcheggioElettriche extends Parcheggio {...}
Automobile a=new Automobile();
Parcheggio p=new ParcheggioElettriche(100);
p.aggiungi(a);
/*
Sorpresa: inserisce Automobile non elettrica in ParcheggioElettriche! Se per
impedirlo si ridefinisce ParcheggioElettriche.aggiungi(Automobile) in modo da
inserire solo Auto elettriche, si viola invece la postcondizione di aggiungi!*/
58