Insertion into a Sorted Threaded Tree
public final class Node {
public /*: claimedby Tree */ Node right;
public /*: claimedby Tree */ Node left;
public /*: claimedby Tree */ Node next;
public /*: claimedby Tree */ int v;
}
public class ThreadedTree
{
private static Node root;
private static Node first;
/*: public static specvar content :: objset;
private vardefs "content ==
{x. rtrancl_pt (% x y. x..left = y | x..right = y) root x}";
invariant "tree [left, right]";
invariant "root ~= null --> (ALL n. n..left ~= root & n..right ~= root)";
invariant "first ~= null --> (ALL n. n..next ~= first)";
invariant "(first,root) : {(x,y). x..next = y}^*";
invariant "ALL x y. x ~= null & y ~= null & (x..right = y | x..left = y) --> y : content";
invariant "ALL x y. x..next = y <->
(x ~= null -->
(x..right = null -->
((EX z. z..left = x) --> y..left = x) &
((ALL z. z..left ~= x) -->
(((ALL z. (left z, x) ~: {(x1,x2). x1..right = x2}^*)) & (y = null) |
(left y, x) : {(x1,x2). x1..right = x2}^*))) &
(x..right ~= null -->
y..left = null & y ~= null & (right x, y) : {(x1, x2). x1..left = x2}^*)) &
(x = null --> y = null)";
invariant "ALL x. x : content & x ~= null & x..next ~= null --> x..v <= x..next..v";
*/
public static void add(Node e)
/*:
requires "e ~: content"
modifies content
ensures "content = old content Un {e}";
*/
{
Node n = root, p = null;
Node pred = null;
Node succ = null;
boolean wentLeft = false;
while (n != null) {
p = n;
if (e.v < n.v) {
wentLeft = true;
succ = n;
n = n.left;
} else {
wentLeft = false;
pred = n;
n = n.right;
}
}
if (p == null) {
root = e;
} else {
if (wentLeft) {
p.left = e;
} else {
p.right = e;
}
}
e.next = succ;
if (pred != null) pred.next = e;
}
}