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.