Singly Linked List Verification
Main points: * new and improved: we define 'reachable' predicate * write code for removeMaybe spec, including loop invariant * write code for remove, including loop invariant
class Node { public /*: claimedby SLL */ Node next; } class SLL { private static Node root; /*: private static specvar reachable :: "obj => obj => bool"; private vardefs "reachable == (% x y. (x,y) : {(u,v). u..next = v}^*)"; public static specvar content :: objset; private vardefs "content == {x. x ~= null & reachable root x}"; invariant tree: "tree [next]"; invariant rootFirst: "root = null | (ALL n. n..next ~= root)"; */ public static void addLast(Node n) /*: requires "n ~: content & n ~= null & n..next = null & (ALL m. m..next ~= n)" modifies content ensures "content = old content Un {n}"; */ { if (root == null) { root = n; n.next = null; return; } Node r = root; while //: inv "r : content" (r.next != null) { r = r.next; } r.next = n; } public static void remove(Node n) /*: requires "n : content" modifies content ensures "content = old content - {n}" */ { if (root == n) { root = root.next; n.next = null; } else { Node r = root; //: assert "reachable r n" while //: inv "r ~= n & r : content & reachable r n" (r.next != n) { r = r.next; } r.next = n.next; n.next = null; } } public static void removeMaybe(Node n) /*: requires "(n : content)" modifies content ensures "content = old content | content = old content - {n}" */ { //: assert "n ~= null"; if (root == n) { root = root.next; n.next = null; } else { Node r = root; while //: inv "r : content | r = null" (r != null && r.next != n) { r = r.next; } if (r != null) { //: assert "r..next = n" r.next = n.next; n.next = null; } } } }