| class CircularList {
/** Construct an empty circular list */
public CircularList()
require true;
ensure empty();
/** Return my number of elements */
public int size()
require true;
ensure size = countElements() && noChange;
/** Insert el as a new first element */
public void insertFirst(Object el)
require !full();
ensure !empty() && isCircular() && isFirst(el);
/** Insert el as a new last element */
public void insertLast(Object el)
require !full();
ensure !empty() && isCircular() && isLast(el);
/** Delete my first element */
public void deleteFirst()
require !empty();
ensure
empty() ||
(isCircular() && isFirst(old retrieveSecond()));
/** Delete my last element */
public void deleteLast()
require !empty();
ensure
empty() ||
(isCircular() && isLast(old retrieveButLast()));
/** Return the first element in the list */
Object retrieveFirst()
require !empty();
ensure isFirst(result) && noChange;
/** Return the last element in the list */
Object retrieveLast()
require !empty();
ensure isLast(result) && noChange;
}
|
|
| | Klassen CircularList med pre- og postbetingelser.
Alle andre detaljer er ignoreret.
Prebetingelser angives med nøgleordet require og postbetingelse med
nøgleordet ensure. Denne syntaks stammer direkte fra Eiffel. Bemærk
venligst at programmet ikke er programmeret i Java, idet Java ikke understøtter
require og ensure. Vi antager at countElement er en operation som rent faktisk tæller antallet af
elementer i Listen. Endvidere at prædikaterne isFirst og isLast er funktioner,
der fortæller hvorvidt et element er det første hhv. det sidste element i listen.
Vi benytter også funktionerne retrieveSecond og retrieveButLast til returnering
af hhv. listens andet og næstsidste element. Bemærk specielt udtryksformen old og noChange. Old foran et udtryk i postbetingelsen beregner udtrykket
i den programtilstand der var gældende umiddelbart før kaldet af operationen. NoChange er opfyldt, hvis
operationen ikke har ændret programtilstanden. (NoChange er med andre ord opfyldt, hvis operationen
er en funktion). Old og NoChange giver kun mening i postbetingelser.
|
