circular-list/java/CircularListPrePost.java - Circular list with preconditions and postconditions.

Lecture 13 - slide 7 : 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() && 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;  
}