Astrazioni sui dati : Ragionare sui Tipi di Dato Astratti Correttezza dell’implementazione



Scaricare 278.5 Kb.
27.11.2017
Dimensione del file278.5 Kb.


Astrazioni sui dati : Ragionare sui Tipi di Dato Astratti


Correttezza dell’implementazione

  • L’implementazione del tipo di dato soddisfa la specifica

  • Rispetto al caso delle procedure stand-alone piu’ complicato

  • Specifica: descrizione astratta degli oggetti + metodi pubblici e le loro proprieta’

  • Implementazione: rappresentazione + implementazione dei metodi



Correttezza dell’implementazione

  • Bisogna provare due cose:

  • La rappresentazione (implementazione) dei dati soddisfa le proprieta’ richieste nella OVERVIEW

  • I metodi soddisfano le loro specifiche (simile al caso delle procedure stand-alone)



Correttezza dell’implementazione

  • Le due cose sono pero’ strettamente correlate

  • La correttezza dei metodi puo’ dipendere da proprieta’ della rappresentazione

  • La correttezza della rappresentazione dipende dai metodi, dato che i metodi creano e modificano gli oggetti



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



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



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



La funzione di astrazione 1

  • la funzione di astrazione cattura l’intenzione del progettista nello scegliere una particolare rappresentazione

  • la funzione di astrazione

  • : C --> A

  • porta da uno stato concreto

    • lo stato di un oggetto della classe C
  • a uno stato astratto

    • lo stato dell’oggetto astratto


Esempio

  • public class IntSet {

  • // OVERVIEW: un IntSet è un insieme modificabile

  • // di interi di dimensione qualunque

  • private Vector els; // la rappresentazione

  • deve mappare vettori di interi in insiemi

  • ([1,2]) = {1,2}

  • ([3,1]) = {1,3}

  • ([1,3,2]) = {1,2,3}



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 )
    • ([1,2]) = {1,2}
    • ([2,1]) = {1,2}


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.



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

  • (c) = { c.els.get(i).intValue() |

  • 0 <= i < c.els.size() }

  • C metavariabile che rappresenta un oggetto generico di IntSet





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

  • (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


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



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

  • // (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)


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



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



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 


L’invariante di rappresentazione di Poly

  • public class Poly {

  • private int[] termini; // la rappresentazione

  • private int deg; // la rappresentazione

  • // la funzione di astrazione

  • // (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



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



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



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


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





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)



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



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



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


Correttezza di IntSet 1

  • public class IntSet {

  • private Vector els; // la rappresentazione

  • // la funzione di astrazione

  • // (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



Correttezza di IntSet 2

  • public class IntSet {

  • private Vector els; // la rappresentazione

  • // la funzione di astrazione

  • // (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


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


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)



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)





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

















Condividi con i tuoi amici:


©astratto.info 2019
invia messaggio

    Pagina principale