Astrazioni sui dati :
Ragionare sui Tipi di Dato
Astratti
1
Correttezza dell’implementazione
L’implementazione del tipo di dato soddisfa la
specifica
 Rispetto al caso delle procedure stand-alone piu’
complicato

1.
2.
Specifica: descrizione astratta degli oggetti +
metodi pubblici e le loro proprieta’
Implementazione: rappresentazione +
implementazione dei metodi
2
Correttezza dell’implementazione
Bisogna provare due cose:
1. La rappresentazione (implementazione) dei dati
soddisfa le proprieta’ richieste nella
OVERVIEW
2. I metodi soddisfano le loro specifiche (simile al
caso delle procedure stand-alone)
3
Correttezza dell’implementazione
Le due cose sono pero’ strettamente correlate
1. La correttezza dei metodi puo’ dipendere da
proprieta’ della rappresentazione
1.
La correttezza della rappresentazione dipende
dai metodi, dato che i metodi creano e
modificano gli oggetti
4
Servono altre informazioni
 Funzione di astrazione: collega la
rappresentazione degli oggetti con la loro
descrizione astratta
 Invariante di rappresentazione: specifica
proprieta’ della rappresentazione degli
oggetti
5
Primo problema
 se vogliamo dimostrare che le implementazioni
dei metodi soddisfano le rispettive specifiche
 l’implementazione utilizza la rappresentazione
– nel caso di IntSet
– private Vector els;
 le specifiche esprimono proprietà dei dati astratti,
ovvero degli insiemi
– nel caso di IntSet
public boolean isIn (int x)
// EFFECTS: se x appartiene a this ritorna
// true, altrimenti false
 Per sapere se l’implementazione la soddisfa devo
sapere come è rappresentato un insieme
6
Cosa manca
 Un modo per mettere in relazione tra loro i due
“insiemi di valori” concreti ed astratti
 valori concreti: stati degli oggetti della classe
(espressi da un insieme di var d’istanza)
 valori astratti: il tipo di dato specificato
 nel caso di IntSet: devo collegare il vettore els
all’insieme di interi che rappresenta
7
La funzione di astrazione 1
 la funzione di astrazione cattura l’intenzione del
progettista nello scegliere una particolare
rappresentazione
 la funzione di astrazione
a : C --> A
porta da uno stato concreto
– lo stato di un oggetto della classe C
a uno stato astratto
– lo stato dell’oggetto astratto
8
Esempio
public class IntSet {
// OVERVIEW: un IntSet è un insieme modificabile
// di interi di dimensione qualunque
private Vector els; // la rappresentazione
 a deve mappare vettori di interi in insiemi
 a ([1,2]) = {1,2}
 a ([3,1]) = {1,3}
 a ([1,3,2]) = {1,2,3}
9
La funzione di astrazione 2
 la funzione di astrazione è generalmente una funzione
molti-a-uno
public class IntSet {
// OVERVIEW: un IntSet è un insieme modificabile
// di interi di dimensione qualunque
private Vector els; // la rappresentazione
– piú stati concreti (vettori di interi) vengono portati nello stesso
stato astratto (insieme )
– a ([1,2]) = {1,2}
–
a ([2,1]) = {1,2}
10
Come definire la funzione di
astrazione?
 il problema è che non abbiamo una rappresentazione
esplicita dei valori astratti (solo specifica informale)
 l’oggetto da rappresentare può essere descritto da un
oggetto astratto tipico della classe dato nella OVERVIEW
della specifica.
 per dare la funzione possiamo usare la notazione
matematica e la notazione del linguaggio di
programmazione con opportune abbreviazioni.
11
La funzione di astrazione di
IntSet
public class IntSet {
// OVERVIEW: un IntSet è un insieme modificabile
// di interi di dimensione qualunque
// un tipico IntSet è {x1, ,xn }
private Vector els; // la rappresentazione
a(c) = { c.els.get(i).intValue() |
0 <= i < c.els.size() }
C metavariabile che rappresenta un oggetto
generico di IntSet
12
La funzione di astrazione di
Poly
public class Poly {
// OVERVIEW: un Poly è un polinomio a
// cofficienti interi non modificabile
// un tipico Poly: c0 + c1*x + c2*x2 + ...
private int[] termini; // la rappresentazione
private int deg; // la rappresentazione

rappresentiamo il polinomio con
– array che ha la dimensione del grado piu’
uno
– l’elemento in posizione n contiene il coefficiente del termine che
ha esponente n (eventualmente 0)
– deg contiene il grado del polinomio
La funzione di astrazione collega l’array al
polinomio
13
La funzione di astrazione di
Poly
public class Poly {
// OVERVIEW: un Poly è un polinomio a
// cofficienti interi non modificabile
// un tipico Poly: c0+ c1 x + c2 x2 + ...
private int[] termini; // la rappresentazione
private int deg; // la rappresentazione
a(c) = c0+ c1 x + c2 x2 + ... tale che
ci = c.termini[i] se 0 <= i < c.termini.length
= 0 altrimenti
 notare che il valore di deg non ha nessuna influenza sulla
funzione di astrazione
– è una informazione derivabile dall’array termini che utilizziamo nello
stato concreto per questioni di efficienza
14
Un altro problema
 non tutti gli stati concreti “rappresentano”
correttamente uno stato astratto
 infatti gli oggetti concreti soddisfano delle
proprieta’, sono costruiti in modo opportuno
 queste proprieta’ servono tipicamente sia per la
correttezza della rappresentazione sia per quella
dei metodi
 Da cosa derivarle
15
Esempio
public class IntSet {
// OVERVIEW: un IntSet è un insieme modificabile
// di interi di dimensione qualunque
// un tipico IntSet è {x1, ,xn }
private Vector els; // la rappresentazione
// la funzione di astrazione
// a(c) = { c.els.get(i).intValue() |
0 <= i < c.els.size() }
 il vettore els potrebbe contenere più occorrenze dello
stesso elemento o contenere valori non di tipo Integer
– questo sarebbe coerente con la funzione di astrazione
– ma non rispecchierebbe la nostra scelta di progetto (riflessa
nell’implementazione dei metodi , vedi per esempio size, remove)
16
L’invariante di rappresentazione
 l’invariante di rappresentazione (rep invariant) è
un predicato
I : C --> boolean
che è vero per gli stati concreti che sono
rappresentazioni legittime di uno stato astratto
 esprime le proprieta’ fondamentali della
rappresentazione (implementazione) degli oggetti
in base alle quali abbiamo definito i metodi
17
L’invariante di rappresentazione
 l’invariante di rappresentazione, insieme alla funzione di
astrazione, riflette le scelte relative alla rappresentazione
– deve essere inserito nella documentazione della implementazione
come commento
 la funzione di astrazione è definita solo per stati concreti
che soddisfano l’invariante
18
L’invariante di rappresentazione
di IntSet
I(c) = c.els != null e
per ogni intero i, c.els.get(i) è un Integer
e per tutti gli interi i,j, tali che
0 <= i < j < c. els.size(),
c.els.get(i).intValue() !=
c.els.get(j).intValue()
 il vettore non deve essere null
 gli elementi del vettore sono tutti distinti
 gli elementi del vettore devono essere Integer
– assunti soddisfatti in a
19
L’invariante di rappresentazione
di Poly
public class Poly {
private int[] termini; // la rappresentazione
private int deg; // la rappresentazione
// la funzione di astrazione
// a(c) = c0 + c1*x + c2*x2 + ... tale che
// ci = c.termini[i] se 0 <= i < c.termini.size()
//
= 0 altrimenti
// l’invariante di rappresentazione:
// I(c) = c.termini != null e
// c.termini.length >= 1 e
// c.deg = c.termini.length-1 e
// c.deg > 0 ==> c.termini[deg] != 0
 Il grado e’ l’esponente massimo con coefficiente non zero
 Il grado (deg) deve essere uguale alla lunghezza dell’array -1
 Il polinomio vuoto e’ rappresentato da un array di un elemento
20
Validita’ dell’invariante
 Come facciamo a dimostrare formalmente
che tutti gli oggetti del nuovo tipo di dato
soddisfano l’invariante?
 Notiamo che, dato che la rappresentazione e’
invisibile, nuovi oggetti possono essere creati solo
coi costruttori e manipolati solo attraverso metodi
pubblici della classe
 Questo suggerisce che per provare la validita’
dell’invariante si puo’ procedere per induzione sul
tipo di dato
21
Induzione sui dati
 induzione sul numero di invocazioni di metodi
usati per produrre il valore corrente dell’oggetto
 Caso Base: dimostriamo che l’invariante vale per
gli oggetti restituiti dai costruttori
22
Caso induttivo
 per tutti i metodi produttori o modificatori separatamente
facciamo vedere che
 assumendo che l’invariante valga (IPOTESI INDUTTIVA)
• per this
• per tutti gli argomenti del tipo
• per gli oggetti del tipo ritornati o modificati da altre chiamate di
metodi interne
 allora quando il metodo termina l’invariante vale
• per this
• per tutti gli argomenti del tipo
• per gli oggetti del tipo ritornati
23
Commenti
 Notate che questo ragionamento induttivo non
sarebbe possibile se la rappresentazione fosse
visibile
 Chi ci garantirebbe che qualcuno non faccia
qualche pasticcio nella rappresentazione
dall’esterno?
 Altro vantaggio di questo stile di
programmazione, piu’ sicuro, piu’ facile ragionare
sulla correttezza
24
IntSet
 Caso Base: il costruttore
 Caso induttivo: per i modificatori insert e
remove assumiamo che this soddisfi
l’invariante e facciamo vedere che la
soiddisfano anche dopo
 Notate che gli altri metodi non modificatori
preservano banalmente l’invariante (non
modificano this)
25
IntSet 1
public class IntSet {
private Vector els; // la rappresentazione
// I(c) = c.els != null e
// per ogni intero i, c.els.get(i) è un Integer
// e per tutti gli interi i,j, tali che
//
0 <= i < j < c. els.size(),
// c.els.get(i).intValue() !=
//
c.els.get(j).intValue()
public IntSet ()
{els = new Vector();}
 il costruttore soddisfa l’invariante perché
restituisce un Vector vuoto (non null)
26
IntSet 2
// I(c) = c.els != null e
// per ogni intero i, c.els.get(i) è un Integer
// e per tutti gli interi i,j, tali che
//
0 <= i < j < c. els.size(),
// c.els.get(i).intValue() !=
//
c.els.get(j).intValue()
public void insert (int x)
{Integer y = new Integer(x);
if (getIndex(y) < 0) els.add(y); }
private int getIndex (Integer x)
// EFFECTS: se x occorre in this ritorna la
// posizione in cui si trova, altrimenti -1
 il metodo insert preserva l’invariante
perché aggiunge x a this solo se x non è
già in this, e lo aggiunge come Integer
27
IntSet 3
// I(c) = c.els != null e
// per ogni intero i, c.els.get(i) è un Integer
// e per tutti gli interi i,j, tali che
//
0 <= i < j < c. els.size(),
// c.els.get(i).intValue() !=
//
c.els.get(j).intValue()
public void remove (int x)
{int i = getIndex(new Integer(x));
if (i < 0) return;
els.set(i, els.lastElement());
els.remove(els.size() - 1);}
 il metodo remove preserva l’invariante
perché rimuove solo
28
Correttezza
 dopo avere dimostrato l’invariante possiamo
provare la correttezza dei metodi
 per ogni metodo separatamente, facciamo vedere
che l’implementazione soddisfa la specifica
– usando il fatto che gli oggetti concreti soddisfano
l’invariante
– usando la funzione di astrazione per collegare dati
concreti ed astratti
– assumendo che le chiamate di altri metodi della classe
interne siano corrette
29
Correttezza di IntSet 1
public class IntSet {
private Vector els; // la rappresentazione
// la funzione di astrazione
// a(c) = { c.els.get(i).intValue() |
0 <= i < c.els.size() }
public IntSet ()
// EFFECTS: inizializza this a vuoto
{els = new Vector();}
 l’astrazione di un vettore vuoto è proprio l’insieme vuoto
30
Correttezza di IntSet 2
public class IntSet {
private Vector els; // la rappresentazione
// la funzione di astrazione
// a(c) = { c.els.get(i).intValue() |
0 <= i < c.els.size() }
public int size ()
// EFFECTS: ritorna la cardinalità di this
{return els.size(); }
 il numero di elementi del vettore è la cardinalità
dell’insieme perché
– la funzione di astrazione mappa gli elementi del vettore in quelli
dell’insieme
– il rep invariant garantisce che non ci sono elementi duplicati in
els
• Possiamo usare size() di Vector
31
Correttezza di IntSet 3
public void remove (int x)
// MODIFIES: this
// EFFECTS: toglie x da this
{int i = getIndex(new Integer(x));
if (i < 0) return;
els.set(i, els.lastElement());
els.remove(els.size() - 1);}
 se x non occorre nel vettore non fa niente
– corretto perché in base alla funzione di astrazione x non
appartiene all’insieme
 se x occorre nel vettore lo rimuove
– e quindi in base alla funzione di astrazione x non
appartiene all’insieme modificato
32
Correttezza di IntSet 4
public void remove (int x)
// MODIFIES: this
// EFFECTS: toglie x da this
{int i = getIndex(new Integer(x));
if (i < 0) return;
els.remove(i);}
 Il rep invariant garantisce che non ci sono elementi
duplicati (getIndex ritorna l’unico indice in cui occorre
l’elemento se compare)
33
Eccezioni
 L’invariante garantisce anche che il vettore
non sia null
 Di conseguenza nei metodi, quando si
accede al vettore, non viene sollevata una
eccezione (che sarebbe sbagliata, perche’
non prevista nella specifica)
34
Come scegliere l’invariante?
 L’invariante riflette le scelte fatte nella rappresentazione
 Deve valere per tutti gli oggetti del tipo (ragionando in
modo induttivo)
 Deve contenere abbastanza informazione per derivare le
proprieta’ richieste nella specifica, sia dei dati che dei metodi
 Per esempio: per la correttezza di remove e size e’
necessario sapere che nel vettore non ci sono occorrenze
multiple (queste condizioni sono esattamente catturate dal
rep invariant)
35
Invariante e f di astrazione
 Devono sempre essere inserite come commento
all’implementazione
 Sono fondamentali per ragionare sulla correttezza
dell’implementazione del tipo di dato astratto
 Possono anche essere implementate ed utilizzate da
programmi test per verificare le proprieta’ a run-time
36
Funzione di astrazione
 non avendo una rappresentazione esplicita dei valori
astratti, possiamo rappresentarli come stringhe
 a questo punto, possiamo implementare la funzione di
astrazione, che è esattamente il metodo toString
– utile per stampare valori astratti
// a(c) = { c.els.get(i).intValue() |
0 <= i < c.els.size() }
37
toString per IntSet
// a(c) = { c.els.get(i).intValue() |
0 <= i < c.els.size() }
public String toString ()
{String s = "{";
for (int i = 0; i < els.size() - 1; i++) {
s = s + els.get(i).toString() + ","; }
if (els.size() > 0) {
s = s + els.get(els.size() - 1).toString(); }
s = s + "}";
return (s);}
38
Invariante di rappresentazione
 Usiamo un metodo repOk che verifica l’invariante pubblico perché
deve poter essere chiamato da fuori della sua classe
 ha sempre la seguente specifica
public boolean rep0k ()
// EFFECTS: ritorna true se il rep invariant
// vale per this, altrimenti ritorna false
39
repOK
 può essere usato da programmi di test per
verificare se una implementazione preserva
l’invariante
 può essere usato dentro le implementazioni di
costruttori e metodi
– creatori, modificatori e produttori dovrebbero chiamarlo
prima di ritornare per assicurarsi che per l’oggetto
costruito o modificato vale l’invariante
• per esempio, dovrebbero chiamarlo insert e remove di
IntSet, add, mul, minus di Poly
 se l’invariante non vale si dovrebbe sollevare
FailureException
40
repOK per IntSet
public class IntSet {
private Vector els;
// la
rappresentazione
// I(c) = c.els != null e
// per ogni intero i, c.els.get(i) è un
Integer
// e per tutti gli interi i,j, tali che
//
0 <= i < j < c. els.size(),
// c.els.get(i).intValue() !=
//
c.els.get(j).intValue()
41
repOK per IntSet
public boolean repOk() {
if (els == null) return false;
for (int i = 0; i < els.size(); i++) {
Object x = els.get(i);
if (! (x instanceof Integer)) return false;
for (int j = i + 1; j < els.size(); j++)
if (x.equals (els.get(j))) return false; }
return true; }
42