circular-list/java/CircularListInvariant.java - Circular list with a class invariant.

Lecture 13 - slide 21 : 32 Program 1

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