Insertion and Removal from a Sorted List
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;
}
}
}