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