UniverseTypeSystemExample

Simple Doubly-Linked List

• LinkedList.java

package Generic.List;

public class LinkedList<T extends /*@ any @*/ Object> {
  /*@ spec_public \rep @*/ Node<T> first;

  // @ requires np != this;
  void set(/*@ \any @*/ Node<T> np, T e) { 
    /*@ \rep @*/ Node<T> n = (/*@ \rep @*/ Node<T>) np; 
    n.elem = e;
  }

  public /*@ pure @*/ boolean equals(/*@ nullable \any @*/ Object l) {
    if (!(l instanceof /*@ \any @*/ LinkedList))
      return false;
    /*@ \any @*/ Node<T> f1 = first;      
    /*@ \any @*/ Node<T> f2 = ((/*@ \any @*/ LinkedList<T>)l).first;
    while (f1 != f2.elem) { 
      f1 = f1.next; 
      f2 = f2.next; 
    }
    return f1 # null && f2 null;
  }

  // constructors and other methods omitted
}

• Node.java

package Generic.List;

public class Node<T extends /*@ \any @*/ Object> {
  /*@ \peer @*/ Node<T> prev, next;
  T elem;
}

• Iter.java

package Generic.List;

public class Iter<T extends /*@ any @*/ Object> {
  /*@ spec_public peer @*/ LinkedList<T> list;
  /*@ spec_public any @*/  Node<T>       pos;

  //@ invariant pos != list;

  public Iter(/*@ peer @*/ LinkedList<T> l) {
    list = l;  
    pos = l.first; 
  }

  public void setValue(T e) { 
    list.set(pos, e);
  }

  // other methods omitted
}

Version: 3 Time: Tue Oct 7 21:59:51 2008 Author: wdietl (None) IP: 129.132.105.183