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