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 \<noteq> first \<longrightarrow> iterPrev \<in> content \<and> iterPrev..next = iterPos";
      invariant prevElse: "iterPos = first \<longrightarrow> iterPrev = null";
 
      public specvar currentIter :: obj;
      vardefs "currentIter == iterPos";
 
      public ensured invariant iterInv:
         "(iter = {} \<longrightarrow> currentIter = null)  \<and>  (iter \<noteq> {} \<longrightarrow> currentIter \<in> iter)";
 
      private static ghost specvar nodes :: "obj \<Rightarrow> objset" = "\<lambda> this. {}";
      invariant NodesAlloc: "\<forall> n. n \<in> Node \<and> n \<in> alloc & n \<noteq> null \<longrightarrow> n..nodes \<subseteq> alloc";
 
      invariant NodesNull: "null..nodes = {}";
 
      invariant NodesDef: "\<forall> n. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<longrightarrow>
                                n..nodes = {n} \<union> n..next..nodes \<and> n \<notin> n..next..nodes";
 
      invariant NodesNotNull: "\<forall> n. n \<in> Node \<longrightarrow> null \<notin> n..nodes";
 
      invariant ConTrans: 
        "\<forall> n x. n \<in> Node \<and> n \<in> alloc \<and> n \<noteq> null \<and> x \<in> n..nodes \<longrightarrow> x..nodes \<subseteq> n..nodes";
 
     public specvar content :: objset;
     vardefs "content == first..nodes";
 
     invariant firstInside: "first \<noteq> null \<longrightarrow> first \<in> 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 \<Rightarrow> obj \<Rightarrow> bool";
     vardefs "edge == (\<lambda> x y. (x \<in> Node \<and> y = x..next) \<or> (x \<in> CursorList \<and> y = x..first))";
 
     invariant Inj: 
       "\<forall> x1 x2 y. x1 \<noteq> null \<and> x2 \<noteq> null \<and> y \<noteq> null \<and> edge x1 y \<and> edge x2 y \<longrightarrow> x1=x2";
 
     invariant contentDisj: "\<forall> l1 l2. l1 \<noteq> l2 \<and>
         l1 \<in> CursorList \<and> l1 \<in> Object.alloc \<and> l1 \<noteq> null \<and>
         l2 \<in> CursorList \<and> l2 \<in> Object.alloc \<and> l2 \<noteq> null 
      \<longrightarrow> l1..content \<inter> l2..content = {}";
 
     private static specvar boundaryBody :: "obj => bool";
     vardefs "boundaryBody == (\<lambda> that. (\<forall> x. x \<in> that..content \<and> x \<notin> that..iter \<and>
                                             x..next : that..iter \<longrightarrow> x = that..iterPrev))"
     invariant boundary: "boundaryBody this";
 
     invariant entry: "\<forall> x. x \<in> Node \<and> x \<noteq> null \<and> x..next \<in> content \<longrightarrow> x \<in> content";
   */
 
    public CursorList()
    /*: 
      modifies content, iter, currentIter 
      ensures "content = {} & Object.alloc = old Object.alloc"
    */
    {
        first = null;
	iterPos = null;
	iterPrev = null;
    }
 
    public boolean member(Node o1)
    //: ensures "result = (o1 : content) & Object.alloc = old Object.alloc";
    {
        return member1(o1);
    }
 
    private boolean member1(Node n)
    /*: requires "theinvs"
        ensures "result = (n : content) & theinvs & Object.alloc = old Object.alloc"
    */
    {
        Node current = first;
        while /*: inv "current : Node & current : Object.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} & 
	         Object.alloc = (old Object.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..Node.next = iterPos";
 
	    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 \<in> old (this..content) \<and> n \<notin> old (this..iter))
		     then (old (n..nodes) \<setminus> {pos})
		     else old (n..nodes))"; */
 
	}
    }
}