LARA

public /*: claimedby CircularList */ class Node {
    public Node next;
    public Node prev;
    public Object data;
 
    /*:
      public ghost specvar next1 :: obj = "null";
    */
}
 
class CircularList
{
    private static Node first;
    private static Node last;
 
    /*:
      public static specvar content :: objset;
      vardefs "content == {d. EX n. n : nodes & n..data = d}";
 
      static specvar nodes :: objset;
      vardefs "nodes == {x. x \<noteq> null \<and> (first,x) \<in> {(v,w). v..next1=w}^*}";
 
     private static specvar isLast :: "obj \<Rightarrow> bool";
     vardefs "isLast == (\<lambda> x. (first,x) \<in> {(v,w). v..next1=w}^* \<and>
                              x \<noteq> null \<and> x..next1 = null)";
 
     invariant lastIsLast: "first \<noteq> null \<longrightarrow> isLast last";
 
     invariant isTree: "tree [next1]";
 
     invariant firstIsolated: "first ~= null --> (ALL n. n : nodes --> n..next1 ~= first)";
 
     invariant nextDef: "\<forall> x y. x..next = y \<longrightarrow>
         ((x \<notin> nodes \<longrightarrow> y = null) \<and>
	  (x = last \<longrightarrow> y = first) \<and>
	  (x \<in> nodes \<and> x \<noteq> last \<longrightarrow> y = x..next1))"
 
     invariant prevDef: "\<forall> x y. x..prev = y \<longrightarrow>
         ((x \<notin> nodes \<longrightarrow> y = null) \<and>
	  (x = first \<and> first \<noteq> null \<longrightarrow> y = last) \<and>
	  (x \<in> nodes \<and> x \<noteq> first \<longrightarrow> y..next1 = x))"
 
     invariant nextNeverNull: "\<forall> x. x \<in> nodes \<longrightarrow> x..next \<noteq> null";
 
     invariant prevNeverNull: "\<forall> x. x \<in> nodes \<longrightarrow> x..prev \<noteq> null";
 
     invariant next1isolated: 
     "\<forall> n. n \<noteq> null \<and> n \<notin> nodes \<longrightarrow> 
     n..next1 = null \<and> (\<forall> x. x..next1 \<noteq> n)";
 
     invariant noDups: "ALL m n. m : nodes & n : nodes & m..data = n..data --> m = n";
 
    */
 
    public static void add(Object data)
    /*: requires "data ~: content"
        modifies content
        ensures "content = old content \<union> {data}"
    */
    {
	Node n = new Node();
	n.data = data;
	addNode(n);
    }
 
    private static void addNode(Node n)
    /*: requires "n..data ~: content & n \<notin> nodes \<and> n \<noteq> null \<and> n..next = null \<and> (\<forall> x. x..next \<noteq> n) & theinvs"
        modifies content, nodes, first, last, next, prev, next1
        ensures "nodes = old nodes Un {n} &
	         content = old content Un {n..data} & theinvs"
    */
    {
	if (first==null) {
	    first = n;
	    n.next = n;
	    n.prev = n;
	    last = n;
	    //: "n..next1" := "null";
	} else {
	    if (first.next==first) {
		last = n;
	    }
	    n.next = first.next;
	    first.next.prev = n;
	    //: "n..next1" := "first..next1";
	    first.next = n;
	    n.prev = first;
	    //: "first..next1" := "n";	    
	}
	 //: noteThat inserted: "nodes = old nodes Un {n}";
    }
 
    public static void remove(Object data)
    /*: modifies content
        ensures "content = old content - {data}"
    */
    {
	Node n = getNode(data);
 
	if (n != null) {
	    removeNode(n);
	}
    }
 
    private static Node getNode(Object data)
    /*: requires "theinvs"
        ensures "comment ''nodeFound'' 
                 (result ~= null --> result : nodes & result..Node.data = data) &
		 comment ''nodeNotFound'' (result = null --> data ~: content)"
     */
    {
	if (first == null) {
	    return null;
	}
 
	Node curr = first;
	//: ghost specvar rnodes :: objset;
 
	//: "rnodes" := "{x. x ~= null & (curr,x) : {(v,w). v..next1=w}^*}";
 
	while /*: inv "comment ''inRest''
		       (ALL n. n : nodes & n..Node.data = data --> n : rnodes) &
		       comment ''inNodes'' (curr : nodes) &
		       comment ''rNodesDef''
		       (rnodes = {x. x ~= null & (curr,x) : {(v,w). v..next1=w}^*})" */
	    (true) {
	    if (curr.data == data) {
		return curr;
	    }
	    if (curr == last) {
		//: note notInRest: "ALL n. n : rnodes --> n..Node.data ~= data";
		return null;
	    }
	    curr = curr.next;
	    //: "rnodes" := "{x. x ~= null & (curr,x) : {(v,w). v..next1=w}^*}";
	}
    }
 
    private static void removeNode(Node n)
    /*: requires "n : nodes & theinvs"
        modifies content, nodes, first, last, next, prev, next1
        ensures "comment ''nodeRemoved'' (nodes = old nodes - {n}) & 
	         comment ''dataRemoved'' (content = old content - {n..data}) &
		 theinvs"
    */
    {
	if (first.next==first) {
	    first = null;
	    n.next = null;
	    n.prev = null;
	    last = null;
	} else {
	    Node nxt = n.next;
	    Node prv = n.prev;
	    prv.next = nxt;
	    nxt.prev = prv;
	    n.next = null;
	    n.prev = null;
	    //: "n..next1" := "null";
	    if (n==first) {
		first = nxt;
	    } else {
		if (n==last) {
		    //: "prv..next1" := "null";
		    last = prv;
		} else {
		    //: "prv..next1" := "nxt";
		}
	    }
	}
	//: note removed: "nodes = old nodes - {n}";
    }
}