Insertion into a Tree with Parent Pointers
public final class Node {
public /*: claimedby Tree */ Node left;
public /*: claimedby Tree */ Node right;
public /*: claimedby Tree */ Node parent;
public /*: claimedby Tree */ int v;
}
public class Tree
{
private static Node root;
/*: public static specvar content :: objset;
private vardefs "content ==
{x. x ~= null &
(root,x) : {(x,y). x..left = y | x..right = y}^*}";
invariant TreeInv: "tree [left, right]";
invariant RootInv: "root = null |
(ALL n. n..left ~= root & n..right ~= root)";
invariant ContentInv:
"ALL x. x ~: content & x ~= null -->
(x..left = null & x..right = null &
(ALL y. y..left ~= x & y..right ~= x))";
invariant ParentInv:
"ALL x y. parent x = y -->
((x ~: content | x = root) --> y = null) &
(x : content & x ~= root --> y ~= null &
(y..left = x | y..right = x))";
*/
public static void add(Node e)
/*:
requires "e ~= null & e ~: content"
modifies content
ensures "content = old content Un {e}";
*/
{
Node n = root, p = null;
boolean wentLeft = false;
while /*: inv "((p = null & n = null) --> root = null) &
(p ~= null --> p : content) &
(n ~= null --> n : content) &
(p ~= null & wentLeft --> p..left = n) &
(p ~= null & ~wentLeft --> p..right = n)"
*/
(n != null) {
p = n;
if (e.v < n.v) {
wentLeft = true;
n = n.left;
} else {
wentLeft = false;
n = n.right;
}
}
if (p == null) {
root = e;
} else {
e.parent = p;
if (wentLeft) {
p.left = e;
} else {
p.right = e;
}
}
}
}