Differences
This shows you the differences between two versions of the page.
— |
sizelist.java [2009/01/30 13:07] (current) wies created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== Insertion and Removal from a List with Size Field ====== | ||
+ | <code java> | ||
+ | class Node { | ||
+ | public /*: claimedby SizeList */ Node next; | ||
+ | } | ||
+ | |||
+ | class SizeList { | ||
+ | private static Node root; | ||
+ | private static int size; | ||
+ | /*: | ||
+ | public static specvar content :: objset; | ||
+ | vardefs "content == {n. n ~= null & (root,n) : {(u,v). u..next=v}^*}"; | ||
+ | invariant sizeInv: "size = cardinality content"; | ||
+ | invariant treeInv: "tree [next]"; | ||
+ | invariant rootInv: "root ~= null --> (ALL n. n..next ~= root)"; | ||
+ | invariant noNextInv: "ALL x. x ~= null & x ~: content --> x..next = null"; | ||
+ | |||
+ | */ | ||
+ | |||
+ | public static void add(Node x) | ||
+ | /*: requires "x ~= null & x ~: content" | ||
+ | modifies content | ||
+ | ensures "content = old content Un {x}" */ | ||
+ | { | ||
+ | x.next = root; | ||
+ | root = x; | ||
+ | size = size + 1; | ||
+ | } | ||
+ | |||
+ | public static void remove(Node x) | ||
+ | /*: requires "x : content" | ||
+ | modifies content | ||
+ | ensures "content = old content - {x}" | ||
+ | */ | ||
+ | { | ||
+ | Node e = root; | ||
+ | Node prev = null; | ||
+ | while (e != x) { | ||
+ | prev = e; | ||
+ | e = e.next; | ||
+ | } | ||
+ | if (prev == null) { | ||
+ | root = e.next; | ||
+ | } else { | ||
+ | prev.next = e.next; | ||
+ | } | ||
+ | e.next = null; | ||
+ | size = size - 1; | ||
+ | } | ||
+ | } | ||
+ | </code> |