Play audio slide show -- Keyboard shortcut: 'x'  Lecture overview -- Keyboard shortcut: 'u'  Previous page: Klasseinvarianter -- Keyboard shortcut: 'p'  Next page: Hvornår skal en invariant være opfyldt? -- Keyboard shortcut: 'n'  Lecture notes - all slides and notes together  Annotated slide -- Keyboard shortcut: 't'  Alphabetic index  Help page about these notes  Course home  Play sound for this slide -- Keyboard shortcut: 'y'    Designkontrakter og ansvarsfordeling - slide 19 : 31

Eksempel på klasseinvariant: CircularList 

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