Specifiche Scopo e significato delle specifiche (1)



Scaricare 1.13 Mb.
02.02.2018
Dimensione del file1.13 Mb.


Specifiche


Scopo e significato delle specifiche (1)

  • Lo scopo di una specifica è di definire il comportamento di un’astrazione. Gli utenti si baseranno su questo comportamento mentre chi implementa l’astrazione dovrà preoccuparsi che venga assicurato.

  • Un’implementazione che fornisce il comportamento descritto si dice che soddisfa la specifica.

  • Definiamo significato di una specifica l’insieme di tutti i moduli di programma che la soddisfano. Lo chiamiamo insieme specificando della specifica.



Scopo e significato delle specifiche (2)

  • Esempio.

  • static int p (int y)

  • // REQUIRES: y > 0

  • // EFFECTS: Returns x such that x > y.

  • Questa specifica è soddisfatta da una procedura p che, quando chiamata con un argomento maggiore di zero, restituisce un valore piú grande del suo argomento. Membri dell’insieme specificando includono

  • static int p (int y) { return y+1; }

  • static int p (int y) { return y*2; }

  • static int p (int y) { return y*3; }

  • Come ogni specifica, questa è soddisfatta da un numero infinito di programmi.



Attributi delle specifiche

  • Una specifica è sufficientemente restrittiva se esclude tutte le implementazioni che sono inaccettabili agli utenti di un’astrazione.

  • Una specifica è sufficientemente generale se non preclude implementazioni accettabili.

  • Una specifica dovrebbe essere chiara cosí che sia facile agli utenti capirla.



Restrittività (1)

  • Una buona specifica dovrebbe essere abbastanza restrittiva da escludere qualunque implementazione che sia inaccettabile agli utenti dell’astrazione. Questa richiesta è alla base di quasi tutti gli usi di specifiche.

  • In generale, discutere se una specifica è sufficientemente restrittiva oppure no implica discutere gli usi che si fanno dei membri dell’insieme specificando.

  • Errori tipici che portano a specifiche restrittive in modo inadeguato: non mettere le richieste necessarie nella clausola REQUIRES.

  • Esempio.

  • Consideriamo tre specifiche per un iteratore elems di un multinsieme (bag) di interi. Un IntBag is come un IntSet tranne che un elemento può occorrervi piú volte.



Restrittività (2)

  • public Iterator elems ( )

  • // EFFECTS: Returns a generator that produces every element of this

  • // (as Integers).

  • public Iterator elems

  • // EFFECTS: Returns a generator that produces every element of this

  • // (as Integers).

  • // REQUIRES: this not be modified while the generator is in use.

  • public Iterator elems ( )

  • // EFFECTS: Returns a generator that produces every element of this

  • // (as Integers), in arbitrary order. Each element is produced exactly

  • // the number of times it occurs in this

  • // REQUIRES: this not be modified while the generator is in use.



Restrittività (3)

  • La prima specifica non tiene conto di quello che può capitare se il bag è cambiato mentre il generatore restituito da elems è in uso e quindi consente implementazioni che danno comportamenti completamente differenti a seconda che il cambiamento del bag influenzi o no il valore restituito.

  • Un modo di trattare il problema è di richiedere che il bag non sia cambiato fintantoché il generatore è in uso, come viene fatto nella seconda specifica.

  • Questa specifica può ancora non essere sufficientemente restrittiva perché non vincola l’ordine in cui gli elementi sono restituiti. Sarebbe meglio o definire un ordine o includere la richiesta "in arbitrary order". Inoltre la specifica non chiarisce che cosa si deve fare quando un elemento compare nel bag piú di una volta e non dice neppure esplicitamente che il generatore restituisce solo gli elementi che sono nel bag. La terza specifica corregge queste mancanze.



Restrittività (4)

  • Altri errori sono dovuti alla non identificazione delle eccezioni da segnalare e alla mancata specifica di quello che va fatto in situazioni al confine.

  • Esempio. Consideriamo una procedura indexString that prende stringhe s1 e s2 e, se s1 è una sottostringa di s2, restituisce l’indice a cui il primo carattere di s1 occorre in s2 ( indexString ("ab" , "babc") restituisce 1). Una specifica che contenesse solo questa informazione non sarebbe abbastanza restrittiva perché non spiega che cosa capita se s1 non è una sottostringa di s2 o se occorre piú volte in s2 o se s1 oppure s2 sono vuote. La specifica seguente è abbastanza restrittiva.

  • public static int indexString (String s1, String s2) throws NullPointerException, EmptyException

  • // EFFECTS: If s1 or s2 is null, throws NullPointerException; else if s1

  • // is the empty string, throws EmptyException; else if s1 occurs as a

  • // substring in s2, returns the least index at which s1 occurs; else returns -1.

  • // E.g. indexString("bc", "abcbc") = 1, indexString ("b" , a") = -1

  • //



Generalità

  • Una buona specifica dovrebbe essere abbastanza generale da assicurare che pochi o nessun programma accettabile sia escluso. Anche se programmi accettabili sono esclusi non lo dovrebbero essere i piú desiderabili, ossia i piú efficienti ed eleganti.

  • Esempio. La specifica seguente

  • public static float sqrt (float sq, float e)

  • // REQUIRES: sq >= 0 && e > .001

  • // EFFECTS: Returns rt such that 0 <= (rt*rt - sq) <= e.

  • costringe l’implementatore ad algoritmi che trovano approssimazioni piú grandi o uguali all’effettiva radice quadrata. Il vincolo può portare a una perdita di efficienza.



Specifiche operazionali e definizionali (1)

  • Una specifica definizionale elenca esplicitamente proprietà che i membri dell’insieme specificando devono esibire Un aspecifica operazionale, invece di descrivere le proprietà dei programmi specificandi dà una ricetta per costruirli.

  • Esempio. Prendiamo un programma che cerca un elemento in un array. La prima specifica spiega come implementare la ricerca, mentre la seconda descrive soltanto una proprietà che gli input e gli output devono soddisfare. La specifica definizionale è piú breve e inoltre lascia all’implementatore la scelta di esaminare l’array in un ordine diverso da quelli dal primo all’ultimo elemento.



Specifiche operazionali e definizionali (2)

  • public static int search (int[ ] a, int x) throws NotFoundException, NullPointerException

  • // EFFECTS: If a is null throws NullPointerException else examines

  • // a[0] , a[1] , ….. , in turn and returns the index of the first one

  • // that is equal to x. Signals NotFoundException if none equals x.

  • public static int search (int[ ] a, int x) throws NotFoundException, NullPointerException

  • // EFFECTS: if a is null throws NullPointerException else returns i

  • // such that a[i] = x; signals NotFoundException if there is no such i.



Chiarezza (1)

  • Una buona specifica dovrebbe essere chiara. I fattori che contribuiscono alla chiarezza sono concisione, ridondanza e struttura.

  • La presentazione piú concisa può non essere la migliore, ma è un buon punto di partenza. La ridondanza può essere introdotta se serve a ridurre il rischio di incomprensione o a cogliere errori.

  • Esempio.

  • Consideriamo un programma che prende due insiemi e verifica se uno è un sottoinsieme dell’altro. La prima specifica è precisa ma può lasciare dei dubbi. Con subset si intende sottoinsieme o sottoinsieme proprio? La seconda specifica non lascia dubbi, ma non dice esplicitamente che si vuole un test della proprietà “essere un sottoinsieme”. La terza specifica è la piú soddisfacente.



Chiarezza (2)

  • static boolean subset (IntSet s1, IntSet s2) throws NullPointerException

  • // EFFECTS: If s1 or s2 is null throws NullPointerException else

  • // returns true if s1 is a subset of s2 else returns false.

  • static boolean subset (IntSet s1, Intset s2) throws NullPointerException

  • // EFFECTS: if s1 or s2 is null throws NullPointerException else

  • // returns true if every element of s1 is an element of s2 else returns

  • // false.

  • static boolean subset (IntSet s1, IntSet s2) throws NullPointerException

  • // EFFECTS: If s1 or s2 is null throws NullPointerException else returns

  • // true if s1 is a subset of s2 else returns false, i.e., returns true if every

  • // element of s1 is an element of s2 else returns false.





Condividi con i tuoi amici:


©astratto.info 2019
invia messaggio

    Pagina principale