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))"; */ } } }