Differences
This shows you the differences between two versions of the page.
— |
sortedlist.java [2009/01/30 12:24] (current) wies created |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== Insertion and Removal from a Sorted List ====== | ||
+ | <code java> | ||
+ | class SortedList | ||
+ | /* sorted list */ | ||
+ | { | ||
+ | private static Node first; | ||
+ | |||
+ | /*: | ||
+ | private static specvar reach :: "obj => obj => bool"; | ||
+ | vardefs | ||
+ | "reach == (% a b. rtrancl_pt (% x y. x..next=y) a b)"; | ||
+ | |||
+ | public static specvar content :: objset; | ||
+ | vardefs | ||
+ | "content == {n. n ~= null & (first, n) : {(x,y). x..next = y}^*}"; | ||
+ | |||
+ | invariant "tree [next]"; | ||
+ | |||
+ | invariant "first = null | (ALL n. n..next ~= first)"; | ||
+ | |||
+ | invariant "ALL x n. x ~= null & n ~= null & x..next = n --> n : content"; | ||
+ | |||
+ | invariant "(ALL n. n : content & n..next ~= null --> n..key <= n..next..key)"; | ||
+ | */ | ||
+ | |||
+ | public static void add(Node nn) | ||
+ | /*: requires "nn ~= null & nn ~: content" | ||
+ | modifies content | ||
+ | ensures "content = old content Un {nn}" | ||
+ | */ | ||
+ | { | ||
+ | if (first==null) { | ||
+ | first = nn; | ||
+ | nn.next = null; | ||
+ | return; | ||
+ | } else if (first.key >= nn.key) { | ||
+ | nn.next = first; | ||
+ | first = nn; | ||
+ | return; | ||
+ | } | ||
+ | |||
+ | Node prev = first; | ||
+ | Node current = first.next; | ||
+ | while ((current != null) && (current.key < nn.key)) { | ||
+ | prev = current; | ||
+ | current = current.next; | ||
+ | } | ||
+ | nn.next = current; | ||
+ | prev.next = nn; | ||
+ | } | ||
+ | |||
+ | public static void remove(Node nn) | ||
+ | /*: requires "nn ~= null" | ||
+ | modifies content | ||
+ | ensures "content = old content - {nn}" | ||
+ | */ | ||
+ | { | ||
+ | Node prev = null; | ||
+ | Node current = first; | ||
+ | while ((current != null) && (current.key < nn.key)) { | ||
+ | prev = current; | ||
+ | current = current.next; | ||
+ | } | ||
+ | |||
+ | if (current == nn) { | ||
+ | if (prev != null) { | ||
+ | prev.next = current.next; | ||
+ | } else { | ||
+ | first = current.next; | ||
+ | } | ||
+ | current.next = null; | ||
+ | } | ||
+ | } | ||
+ | } | ||
+ | </code> |