LARA

class Node {
    public Object data;
    public /*: claimedby CursorList */ Node next;
}
 
class CursorList {
   private Node first;
 
   private Node iterPos;
   private Node iterPrev;
 
   /*: 
      invariant prevDef: "iterPos ~= first --> iterPrev : content & iterPrev..next = iterPos";
      invariant prevElse: "iterPos = first --> iterPrev = null";
 
      public specvar currentIter :: obj;
      vardefs "currentIter == iterPos";
 
      public ensured invariant iterInv:
         "(iter = {} --> currentIter = null)  &  (iter ~= {} --> currentIter : iter)";
 
      private static ghost specvar nodes :: "obj => objset" = "\<lambda> this. {}";
      invariant NodesAlloc: "\<forall> n. n : Node & n : alloc & n ~= null --> n..nodes \<subseteq> alloc";
 
      invariant NodesNull: "null..nodes = {}";
 
      invariant NodesDef: "\<forall> n. n : Node & n : alloc & n ~= null -->
                                n..nodes = {n} \<union> n..next..nodes & n ~: n..next..nodes";
 
      invariant NodesNotNull: "\<forall> n. n : Node --> null ~: n..nodes";
 
      invariant ConTrans: 
        "\<forall> n x. n : Node & n : alloc & n ~= null & x : n..nodes --> x..nodes \<subseteq> n..nodes";
 
     public specvar content :: objset;
     vardefs "content == first..nodes";
 
     invariant firstInside: "first ~= null --> first : content";
 
     public specvar iter :: objset;
     vardefs "iter == iterPos..nodes";
 
     public ensured invariant ContentAlloc: "content \<subseteq> alloc";
     public ensured invariant ContentNode: "content \<subseteq> Node";
     public ensured invariant IterSubset: "iter \<subseteq> content";
 
     private static specvar edge :: "obj => obj => bool";
     vardefs "edge == (\<lambda> x y. (x : Node & y = x..next) \<or> (x : CursorList & y = x..first))";
 
     invariant Inj: 
       "\<forall> x1 x2 y. x1 ~= null & x2 ~= null & y ~= null & edge x1 y & edge x2 y --> x1=x2";
 
     invariant contentDisj: "\<forall> l1 l2. l1 ~= l2 &
         l1 : CursorList & l1 : alloc & l1 ~= null &
         l2 : CursorList & l2 : alloc & l2 ~= null 
      --> l1..content \<inter> l2..content = {}";
 
     private static specvar boundaryBody :: "obj => bool";
     vardefs "boundaryBody == (\<lambda> that. (\<forall> x. x : that..content & x ~: that..iter &
                                             x..next : that..iter --> x = that..iterPrev))"
     invariant boundary: "boundaryBody this";
 
     invariant entry: "\<forall> x. x : Node & x ~= null & x..next : content --> x : content";
   */
 
    public CursorList()
    /*: 
      modifies content, iter, currentIter 
      ensures "content = {} & alloc = old alloc"
    */
    {
        first = null;
	iterPos = null;
	iterPrev = null;
    }
 
    public boolean member(Node o1)
    //: ensures "result = (o1 : content) & alloc = old alloc";
    {
        return member1(o1);
    }
 
    private boolean member1(Node n)
    /*: requires "theinvs"
        ensures "result = (n : content) & theinvs & alloc = old alloc"
    */
    {
        Node current = first;
        while /*: inv "current : Node & current : alloc &
                       (n : content) = (n : current..nodes)" */
            (current != null) {
            if (current==n) {
                return true;
            }
            current = current.next;
        }
        return false;
    }
 
    public Node addNew()
    /*: modifies content
        ensures "content = old content Un {result} & 
	         alloc = (old alloc) Un {result}";
    */
    {
	Node n = new Node();
	n.next = first;
	if (iterPos==first) {
	    iterPrev = n;
	}
	//: "n..nodes" := "{n} Un first..nodes";
	first = n;
	return n;
    }
 
    public void initIter()
    /*: modifies iter, currentIter
        ensures "iter = content" */
    {
	iterPos = first;
	iterPrev = null;
    }
 
    public Node nextIter()
    /*: requires "iter ~= {}" 
      modifies iter, currentIter
      ensures "iter = old iter - {result} & 
               result : old iter"
    */
    {
	iterPrev = iterPos;
	iterPos = iterPos.next;
	return iterPrev;
    }
 
    public Node getCurrent()
    //: ensures "result = currentIter" 
    {
	return iterPos;
    }
 
    public boolean lastIter()
    //: ensures "result = (iter = {})"
    {
	return iterPos == null;
    }
 
    public void removeCurrent()
    /*:
     requires "comment ''currentNotNull'' (currentIter ~= null)"
     modifies content, iter, currentIter
     ensures "content = old content \<setminus> {old currentIter} & 
              iter = old iter \<setminus> {old currentIter}" */
    {
	if (iterPos==first) {
	    //: note notNull: "first ~= null";
	    Node n = first;
	    first = first.next;
	    iterPos = first;
	    iterPrev = null;
	    n.next = null;
	    //: "n..nodes" := "{n}";
	} else {
	    //: note prevNext: "iterPrev..next = iterPos";
	    // note ok1: "iterPos ~= first";
 
	    Node pos = this.iterPos;
	    Node n = pos.next;
	    iterPrev.next = n;
	    pos.next = null;
	    iterPos = n;
 
	    /*: "CursorList.nodes" := 
		"\<lambda> n. if n = pos then {pos} else
		    (if (n : old (this..content) & n ~: old (this..iter))
		     then (old (n..nodes) \<setminus> {pos})
		     else old (n..nodes))"; */
 
	}
    }
}