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() && isFirst(el);
// Insert el as a new last element
public void insertLast(Object el)
require !full();
ensure !empty() && isLast(el);
// Delete my first element
public void deleteFirst()
require !empty();
ensure (empty() || isFirst(old retrieveSecond));
// Delete my last element
public void deleteLast()
require !empty();
ensure (empty() || 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;
invariant
!empty() implies isCircular() and
empty() implies (size() = 0);
} |