LARA

class Node {
    public /*: claimedby CircularList */ Node next;
    public /*: claimedby CircularList */ Node prev;
}
 
class CircularList
{
    private static Node first;
    private static Node last;
 
   /*:
     private static ghost specvar next1 :: "obj => obj" = "(\<lambda> x. null)";
 
     public static specvar content :: objset;
     vardefs "content == {x. x ~= null & (first,x) : {(v,w). v..next1=w}^*}";
 
     private static specvar isLast :: "obj => bool";
     vardefs "isLast == (\<lambda> x. (first,x) : {(v,w). v..next1=w}^* &
                              x ~= null & x..next1 = null)";
     invariant lastIsLast: "first ~= null --> isLast last";
 
     invariant firstIsolated: "first ~= null --> (\<forall> n. n..next1 ~= first)";
 
     invariant isTree: "tree [next1]";
 
     invariant nextDef: "\<forall> x y. next x = y -->
         ((x = last --> y = first) &
	  (x : content & x ~= last --> y = x..next1) &
	  (x \<notin> content --> y=null))"
 
     invariant prevDef: "\<forall> x y. prev x = y -->
         ((x \<notin> content --> y = null) &
	  (x = first & first ~= null --> y = last) &
	  (x : content & x ~= first --> y..next1 = x))"
 
     invariant nextNeverNull: "\<forall> x. x : content --> x..next ~= null";
     invariant prevNeverNull: "\<forall> x. x : content --> x..prev ~= null";
 
     invariant next1isolated: "\<forall> n. n ~= null & n \<notin> content --> isolated n";
     private static specvar isolated :: "obj => bool";
     vardefs "isolated == (\<lambda> n. n..next1 = null & (\<forall> x. x ~= null --> x..next1 ~= n))";
   */
 
    public static void add(Node n)
    /*: requires "n \<notin> content & n ~= null & n..next = null & (\<forall> x. x..next ~= n)"
        modifies content
        ensures "content = old content \<union> {n}"
    */
    {
	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: "content = old content Un {n}";
    }
 
    public static void remove(Node n)
    /*: requires "n : content"
        modifies content
        ensures "comment ''removePost'' (content = old content - {n})"
    */
    {
	//: noteThat "first ~= null";
	//: noteThat "n ~= null";
	if (first.next==first) {
	    //: noteThat lone: "n = first";
	    first = null;
	    n.next = null;
	    n.prev = 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";
		}
	    }
	}
    }
}