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;
}