public /*: claimedby BinarySearchTree */ final class Node { public /*: claimedby BinarySearchTree */ Node left; public /*: claimedby BinarySearchTree */ Node right; public /*: claimedby BinarySearchTree */ Node parent; public /*: claimedby BinarySearchTree */ int v; /*: public specvar subtree :: objset; public vardefs "subtree == {n0. n0 \<noteq> null \<and> (this,n0) \<in> {(x,y). x..left=y \<or> x..right=y}^*}"; */ } public class BinarySearchTree { private static Node root; /*: public static specvar content :: objset; private vardefs "content == root..subtree"; invariant TreeInv: "tree [Node.left, Node.right]"; invariant RootInv: "root = null \<or> (\<forall> n. n..left \<noteq> root & n..right \<noteq> root)"; invariant RootParentInv: "root..parent = null"; invariant ContentInv: "\<forall> x. x \<notin> content & x \<noteq> null \<longrightarrow> (x..left = null \<and> x..right = null \<and> (\<forall> y. y..left \<noteq> x \<and> y..right \<noteq> x))"; invariant ParentInv: "\<forall> x y. x..parent = y \<longrightarrow> (x \<notin> content \<longrightarrow> y = null) \<and> (x \<in> content & x \<noteq> root \<longrightarrow> y \<noteq> null \<and> (y..left = x \<or> y..right = x))"; invariant LeftOrderingInv: "\<forall> x y. y \<in> x..left..subtree \<longrightarrow> y..v < x..v"; invariant RightOrderingInv: "\<forall> x y. y \<in> x..right..subtree \<longrightarrow> y..v \<ge> x..v"; */ public static void add(Node e) /*: requires "e \<noteq> null & e \<notin> content" modifies content ensures "content = old content \<union> {e}"; */ { Node n = root, p = null; boolean wentLeft = false; while /*: inv "(p = null \<and> n = null \<longrightarrow> root = null) \<and> (p = null \<longrightarrow> n = root) \<and> (p \<noteq> null \<longrightarrow> p \<in> content) \<and> (n \<noteq> null \<longrightarrow> n \<in> content) \<and> (p \<noteq> null \<and> wentLeft \<longrightarrow> p..left = n) \<and> (p \<noteq> null \<and> \<not> wentLeft \<longrightarrow> p..right = n) \<and> (comment ''WentLeftLInv'' (p \<noteq> null \<and> wentLeft \<longrightarrow> e..v < p..v)) \<and> (comment ''WentRightLInv'' (p \<noteq> null \<and> \<not> wentLeft \<longrightarrow> e..v \<ge> p..v)) \<and> (comment ''LOrderLInv'' (\<forall> x. p \<in> x..left..subtree \<and> p \<noteq> null \<and> p \<noteq> x \<longrightarrow> e..v < x..v)) \<and> (comment ''ROrderLInv'' (\<forall> x. p \<in> x..right..subtree \<and> p \<noteq> null \<and> p \<noteq> x \<longrightarrow> e..v \<ge> x..v))" */ (n != null) { /*: noteThat LSubtree: "ALL x. n : x..Node.left..Node.subtree & p ~= null & p ~= x --> p : x..Node.left..Node.subtree"; */ /*: noteThat RSubtree: "ALL x. n : x..Node.right..Node.subtree & p ~= null & p ~= x --> p : x..Node.right..Node.subtree"; */ /*: noteThat RootNotInLeft: "p = null --> (ALL x. n ~: x..Node.left..Node.subtree)"; */ /*: noteThat RootNotInRight: "p = null --> (ALL x. n ~: x..Node.right..Node.subtree)"; */ /*: noteThat WentLeftSubtree: "wentLeft --> n ~: p..Node.right..Node.subtree"; */ /*: noteThat WentRightSubtree: "~wentLeft --> n ~: p..Node.left..Node.subtree"; */ 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; //: noteThat PNonNull: "p ~= null"; //: noteThat PEDiff: "e ~= p"; //: noteThat SingletonSubtree: "e..Node.subtree = { e }"; if (wentLeft) { p.left = e; //: noteThat WentLeft: "e..Node.v < p..Node.v"; //: noteThat ENotInROfP: "e ~: p..Node.right..Node.subtree"; } else { p.right = e; //: noteThat WentRight: "e..Node.v >= p..Node.v"; //: noteThat ENotInLOfP: "e ~: p..Node.left..Node.subtree"; } /*: noteThat SubtreeRelL0: "ALL x y. y : x..Node.left..Node.subtree --> (y : (fieldRead (old Node.subtree) (x..Node.left)) | y = e)"; */ /*: noteThat SubtreeRelL1: "ALL x. e : x..Node.left..Node.subtree & x ~= p --> p : fieldRead (old Node.subtree) (x..Node.left)"; */ /*: noteThat SubtreeRelR0: "ALL x y. y : x..Node.right..Node.subtree --> (y : (fieldRead (old Node.subtree) (x..Node.right)) | y = e)"; */ /*: noteThat SubtreeRelR1: "ALL x. e : x..Node.right..Node.subtree & x ~= p --> p : fieldRead (old Node.subtree) (x..Node.right)"; */ } } public static boolean contains(Node n) /*: requires "n ~= null" ensures "result = (n : content)" */ { Node curr = root; while /*: inv "(curr ~= null --> curr : content) & (comment ''InContentLInv'' (n : content) = (n : curr..Node.subtree))" */ (curr != null) { if (curr == n) { return true; } else { /*: noteThat SubtreeDef: "(n : curr..Node.subtree) = ((n = curr) | (n : curr..Node.left..Node.subtree) | (n : curr..Node.right..Node.subtree))"; */ if (n.v < curr.v) { curr = curr.left; } else { curr = curr.right; } } } return false; } public static Node extractMax() /*: modifies content ensures "(result = null --> (ALL x. (x ~: content))) & (result ~= null --> content = old content - {result}) & (result ~= null --> (ALL x. x : old content --> result..Node.v >= x..Node.v))" */ { //: private static ghost specvar smaller :: objset; Node curr = root; //: smaller := "{}"; while /*: inv "(curr ~= null --> curr : content) & (curr = null --> curr = root) & (content = smaller Un curr..Node.subtree) & (comment ''SmallerLInv'' (ALL x. x : smaller --> curr..Node.v >= x..Node.v))" */ (curr != null && curr.right != null) { //: smaller := "smaller Un {curr} Un curr..Node.left..Node.subtree"; /*: noteThat SubtreeRRel: "curr..Node.right : curr..Node.right..Node.subtree"; */ curr = curr.right; /*: noteThat SmallerLemma: "ALL x. x : smaller --> curr..Node.v >= x..Node.v" from SmallerLemma, SmallerLInv, SubtreeRRel, LeftOrderingInv, RightOrderingInv; */ } /*: noteThat CurrEq: "curr..Node.v >= curr..Node.v"; */ /*: noteThat CurrRight: "ALL x. x ~: curr..Node.right..Node.subtree"; */ /*: noteThat SubtreeDef: "curr ~= null --> curr..Node.subtree = { curr } Un curr..Node.left..Node.subtree Un curr..Node.right..Node.subtree"; */ /*: noteThat Smallest: "curr ~= null --> (ALL x. x : content --> curr..Node.v >= x..Node.v)"; */ if (curr != null) { remove_int(curr); {//: localize; //: noteThat NodeUnchanged: "Node.v = old Node.v"; /*: noteThat OrderingEnd: "ALL x. x : old content --> curr..Node.v >= x..Node.v" from Smallest, TrueBranch, OrderingEnd, NodeUnchanged; */ } } return curr; } public static Node extractMin() /*: modifies content ensures "(result = null --> (ALL x. (x ~: content))) & (result ~= null --> content = old content - {result}) & (result ~= null --> (ALL x. x : old content --> result..Node.v <= x..Node.v))" */ { //: private static ghost specvar bigger :: objset; Node curr = root; //: bigger := "{}"; while /*: inv "(curr ~= null --> curr : content) & (curr = null --> curr = root) & (content = bigger Un curr..Node.subtree) & (comment ''BiggerLInv'' (ALL x. x : bigger --> curr..Node.v <= x..Node.v))" */ (curr != null && curr.left != null) { //: bigger := "bigger Un {curr} Un curr..Node.right..Node.subtree"; /*: noteThat SubtreeLRel: "curr..Node.left : curr..Node.left..Node.subtree"; */ curr = curr.left; /*: noteThat BiggerLemma: "ALL x. x : bigger --> curr..Node.v <= x..Node.v" from BiggerLemma, BiggerLInv, SubtreeLRel, RightOrderingInv, LeftOrderingInv; */ } //: noteThat CurrEq: "curr..Node.v <= curr..Node.v"; //: noteThat CurrLeft: "ALL x. x ~: curr..Node.left..Node.subtree"; /*: noteThat SubtreeDef: "curr ~= null --> curr..Node.subtree = { curr } Un curr..Node.left..Node.subtree Un curr..Node.right..Node.subtree"; */ /*: noteThat Biggest: "curr ~= null --> (ALL x. x : content --> curr..Node.v <= x..Node.v)"; */ if (curr != null) { remove_int(curr); { //: localize; //: noteThat NodeUnchanged: "Node.v = old Node.v"; /*: noteThat OrderingEnd: "ALL x. x : old content --> curr..Node.v <= x..Node.v" from Biggest, TrueBranch, OrderingEnd, NodeUnchanged; */ } } return curr; } private static Node removeMin(Node n) /*: requires "theinvs & n ~= null & n : content & n..Node.right ~= null" modifies content, "Node.left", "Node.right", "Node.parent", "Node.subtree" ensures "theinvs & content = old content - {result} & result : old content & result ~= n & (ALL y. y : n..Node.left..Node.subtree --> y..Node.v < result..Node.v) & (ALL y. y : n..Node.right..Node.subtree --> result..Node.v <= y..Node.v) & (ALL x. n : x..Node.left..Node.subtree --> result..Node.v < x..Node.v) & (ALL x. n : x..Node.right..Node.subtree --> x..Node.v <= result..Node.v) & Node.v = (old Node.v)" */ { //: private static ghost specvar bigger :: objset; Node e = n.right; //: bigger := "{}"; while /*: inv "e ~= null & e : content & (rtrancl_pt (% x y. x..Node.left = y) (n..Node.right) e) & (n..Node.right..Node.subtree = bigger Un e..Node.subtree) & (comment ''BiggerLInv'' (ALL x. x : bigger --> e..Node.v < x..Node.v)) & (e : n..Node.right..Node.subtree)" */ (e.left != null) { //: bigger := "bigger Un {e} Un e..Node.right..Node.subtree"; /*: noteThat SubtreeRRel: "e..Node.left : e..Node.left..Node.subtree"; */ e = e.left; /*: noteThat BiggerLemma: "ALL x. x : bigger --> e..Node.v < x..Node.v" from BiggerLemma, BiggerLInv, SubtreeRRel, LeftOrderingInv, RightOrderingInv; */ } //: noteThat ELeft: "ALL x. x ~: e..Node.left..Node.subtree"; /*: noteThat SubtreeDef: "e ~= null --> e..Node.subtree = { e } Un e..Node.left..Node.subtree Un e..Node.right..Node.subtree"; */ if (e.parent.left == e) { e.parent.left = e.right; } else { //: noteThat "e..Node.parent..Node.right = e"; e.parent.right = e.right; } if (e.right != null) { e.right.parent = e.parent; } e.parent = null; e.right = null; /*: noteThat SubtreeChange: "ALL x y. y : x..Node.subtree & x ~= e & y ~= e --> y : (fieldRead (old Node.subtree) x)"; */ //: noteThat EIsolated: "ALL x. x ~= e --> e ~: x..Node.subtree"; //: noteThat ENoChildren: "e..Node.subtree = { e }"; /*: noteThat ENRel: "ALL x. n : x..Node.left..Node.subtree --> e : (fieldRead (old Node.subtree) (fieldRead (old Node.left) x))"; */ return e; } private static Node removeMax(Node n) /*: requires "theinvs & n ~= null & n : content & n..Node.left ~= null" modifies content, "Node.left", "Node.right", "Node.parent", "Node.subtree" ensures "theinvs & content = old content - {result} & result : old content & result ~= n & (ALL x. x : n..Node.left..Node.subtree --> x..Node.v <= result..Node.v) & (ALL x. x : n..Node.right..Node.subtree --> x..Node.v >= result..Node.v)" */ { //: private static ghost specvar smaller :: objset; Node e = n.left; //: smaller := "{}"; while /*: inv "e ~= null & e : content & (rtrancl_pt (% x y. x..Node.right = y) (n..Node.left) e) & (n..Node.left..Node.subtree = smaller Un e..Node.subtree) & (comment ''SmallerLInv'' (ALL x. x : smaller --> e..Node.v >= x..Node.v)) & (e : n..Node.left..Node.subtree)" */ (e.right != null) { //: smaller := "smaller Un {e} Un e..Node.left..Node.subtree"; /*: noteThat SubtreeRRel: "e..Node.right : e..Node.right..Node.subtree"; */ e = e.right; /*: noteThat SmallerLemma: "ALL x. x : smaller --> e..Node.v >= x..Node.v" from SmallerLemma, SmallerLInv, SubtreeRRel, LeftOrderingInv, RightOrderingInv; */ } //: noteThat ERight: "ALL x. x ~: e..Node.right..Node.subtree"; /*: noteThat SubtreeDef: "e ~= null --> e..Node.subtree = { e } Un e..Node.left..Node.subtree Un e..Node.right..Node.subtree"; */ if (e.parent.right == e) { e.parent.right = e.left; } else { e.parent.left = e.left; } if (e.left != null) { e.left.parent = e.parent; } e.parent = null; e.left = null; /*: noteThat SubtreeChange: "ALL x y. y : x..Node.subtree & x ~= e & y ~= e --> y : (fieldRead (old Node.subtree) x)"; */ //: noteThat EIsolated: "ALL x. x ~= e --> e ~: x..Node.subtree"; //: noteThat ENoChildren: "e..Node.subtree = { e }"; return e; } private static void swap(Node toRemove, Node toAdd) /*: requires "toRemove ~= null & toRemove : content & toAdd ~= null & toAdd ~: content & (comment ''LOPreS'' (ALL x. x : toRemove..Node.left..Node.subtree --> x..Node.v < toAdd..Node.v)) & (comment ''ROPreS'' (ALL x. x : toRemove..Node.right..Node.subtree --> toAdd..Node.v <= x..Node.v)) & (comment ''LOPreR'' (ALL x. toRemove : x..Node.left..Node.subtree --> toAdd..Node.v < x..Node.v)) & (comment ''ROPreR'' (ALL x. toRemove : x..Node.right..Node.subtree --> x..Node.v <= toAdd..Node.v)) & theinvs" modifies content, root, "Node.subtree", "Node.parent", "Node.right", "Node.left" ensures "content = old content - {toRemove} Un {toAdd} & Node.v = (old Node.v) & theinvs" */ { //: noteThat toAddIsolatedL: "ALL x. x..Node.left ~= toAdd"; //: noteThat toAddIsolatedR: "ALL x. x..Node.right ~= toAdd"; if (toRemove.parent == null) { //: noteThat "root = toRemove"; root = toAdd; } else { //: noteThat HasParent: "toRemove..Node.parent ~= null"; if (toRemove.parent.left == toRemove) { /*: noteThat toRemoveID: "toRemove..Node.parent..Node.left = toRemove"; */ toRemove.parent.left = toAdd; } else { /*: noteThat toRemoveID: "toRemove..Node.parent..Node.right = toRemove"; */ toRemove.parent.right = toAdd; } } toAdd.parent = toRemove.parent; toRemove.parent = null; toAdd.left = toRemove.left; toRemove.left = null; toAdd.right = toRemove.right; toRemove.right = null; if (toAdd.left != null) { toAdd.left.parent = toAdd; } if (toAdd.right != null) { toAdd.right.parent = toAdd; } /*: noteThat toRemoveSubtree: "toRemove..Node.subtree = { toRemove }"; */ /*: noteThat LORemovedR: "ALL y. y : toRemove..Node.left..Node.subtree --> y..Node.v < toRemove..Node.v"; */ /*: noteThat RORemovedR: "ALL y. y : toRemove..Node.right..Node.subtree --> toRemove..Node.v <= y..Node.v"; */ /*: noteThat LORemovedS: "ALL x. toRemove : x..Node.left..Node.subtree --> toRemove..Node.v < x..Node.v"; */ /*: noteThat RORemovedS: "ALL x. toRemove : x..Node.right..Node.subtree --> x..Node.v <= toRemove..Node.v"; */ /*: noteThat SubtreeChange: "ALL x y. y : x..Node.subtree & x ~= toAdd & y ~= toAdd --> y : (fieldRead (old Node.subtree) x)"; */ /*: noteThat SubtreeSwapL: "toAdd..Node.left..Node.subtree = (fieldRead (old Node.subtree) (fieldRead (old Node.left) toRemove))"; */ /*: noteThat SubtreeSwapR: "toAdd..Node.right..Node.subtree = (fieldRead (old Node.subtree) (fieldRead (old Node.right) toRemove))"; */ /*: noteThat SubtreeSwapPL: "ALL x. toAdd : x..Node.left..Node.subtree --> toRemove : (fieldRead (old Node.subtree) (fieldRead (old Node.left) x))" */ /*: noteThat SubtreeSwapPR: "ALL x. toAdd : x..Node.right..Node.subtree --> toRemove : (fieldRead (old Node.subtree) (fieldRead (old Node.right) x))"; */ /*: noteThat LOSwappedR: "ALL y. y : toAdd..Node.left..Node.subtree --> y..Node.v < toAdd..Node.v"; */ /*: noteThat LOSwappedS: "ALL x. toAdd : x..Node.left..Node.subtree --> toAdd..Node.v < x..Node.v" from LOSwappedS, HasParent, LOPreR, SubtreeSwapPL; */ //: noteThat NEq: "toAdd ~= toRemove"; /*: noteThat SwappedSubtree: "ALL x. x : toAdd..Node.subtree & x ~= toAdd --> x : fieldRead (old Node.subtree) toRemove"; */ /*: noteThat LOPart: "ALL x y. y : x..Node.left..Node.subtree & x ~= toAdd & y ~= toAdd & x ~= toRemove & y ~= toRemove --> y..Node.v < x..Node.v" from LOPart, LeftOrderingInv, SubtreeChange, NEq, toAddIsolatedL, toRemoveID, SwappedSubtree; */ /*: noteThat LOEnd: "theinv LeftOrderingInv" from LOEnd, LOPart, LORemovedR, LOSwappedR, LORemovedS, LOSwappedS, NEq; */ /*: noteThat ROSwappedR: "ALL y. y : toAdd..Node.right..Node.subtree --> toAdd..Node.v <= y..Node.v"; */ /*: noteThat ROSwappedS: "ALL x. toAdd : x..Node.right..Node.subtree --> x..Node.v <= toAdd..Node.v"; */ /*: noteThat ROPart: "ALL x y. y : x..Node.right..Node.subtree & x ~= toAdd & y ~= toAdd & x ~= toRemove & y ~= toRemove --> x..Node.v <= y..Node.v" from ROPart, RightOrderingInv, SubtreeChange, NEq, toAddIsolatedR, toRemoveID, SwappedSubtree; */ /*: noteThat ROEnd: "theinv RightOrderingInv" from ROEnd, ROPart, RORemovedR, ROSwappedR, RORemovedS, ROSwappedS, NEq; */ } public static void remove(Node e) /*: requires "e ~= null & e : content" modifies content ensures "(content = old content - {e}) & Node.v = (old Node.v)" */ { remove_int(e); } private static void remove_int(Node e) /*: requires "e ~= null & e : content & theinvs" modifies content, "Node.subtree", root, "Node.parent", "Node.right", "Node.left" ensures "(content = old content - {e}) & Node.v = (old Node.v) & theinvs" */ { if (e.left == null) { if (e.right == null) { // e has no children if (e.parent == null) { // e is the root node root = null; } else if (e.parent.left == e) { // e is a left child e.parent.left = null; } else { // e is a right child e.parent.right = null; } } else { // e has a right child but no left child if (e.parent == null) { // e is the root node root = e.right; } else { if (e.parent.left == e) { // e is a left child e.parent.left = e.right; } else { // e is a right child e.parent.right = e.right; } } e.right.parent = e.parent; e.right = null; } e.parent = null; //: noteThat LOESubtree: "e..Node.subtree = { e }"; //: noteThat EIsolated: "ALL x. x ~= e --> e ~: x..Node.subtree"; //: noteThat ENotLeft: "ALL x. x..Node.left ~= e"; //: noteThat ENotRight: "ALL x. x..Node.right ~= e"; //: noteThat ENoParent: "e..Node.parent = null"; /*: noteThat SubtreeChangeL: "ALL x y. y : x..Node.left..Node.subtree & y ~= e --> y : (fieldRead (old Node.subtree) (fieldRead (old Node.left) x))"; */ /*: noteThat LOPart: "ALL x y. y : x..Node.left..Node.subtree & y ~= e --> y..Node.v < x..Node.v"; */ /*: noteThat LOEnd: "theinv LeftOrderingInv" from LOPart, EIsolated, ENotLeft, ENoParent; */ /*: noteThat SubtreeChangeR: "ALL x y. y : x..Node.right..Node.subtree & y ~= e --> y : (fieldRead (old Node.subtree) (fieldRead (old Node.right) x))"; */ /*: noteThat ROPart: "ALL x y. y : x..Node.right..Node.subtree & y ~= e --> x..Node.v <= y..Node.v"; */ /*: noteThat ROEnd: "theinv RightOrderingInv" from ROPart, EIsolated, ENotRight, ENoParent; */ } else { if (e.right == null) { // e has a left child but no right child if (e.parent == null) { // e is the root node root = e.left; } else { if (e.parent.left == e) { // e is a left child e.parent.left = e.left; } else { // e is a right child e.parent.right = e.left; } } e.left.parent = e.parent; e.left = null; e.parent = null; //: noteThat LOESubtree: "e..Node.subtree = { e }"; /*: noteThat EIsolated: "ALL x. x ~= e --> e ~: x..Node.subtree"; */ //: noteThat ENotLeft: "ALL x. x..Node.left ~= e"; //: noteThat ENotRight: "ALL x. x..Node.right ~= e"; //: noteThat ENoParent: "e..Node.parent = null"; /*: noteThat SubtreeChangeL: "ALL x y. y : x..Node.left..Node.subtree & y ~= e --> y : (fieldRead (old Node.subtree) (fieldRead (old Node.left) x))"; */ /*: noteThat LOPart: "ALL x y. y : x..Node.left..Node.subtree & y ~= e --> y..Node.v < x..Node.v"; */ /*: noteThat LOEnd: "theinv LeftOrderingInv" from LOEnd, LOPart, EIsolated, ENotLeft, ENoParent; */ /*: noteThat SubtreeChangeR: "ALL x y. y : x..Node.right..Node.subtree & y ~= e --> y : (fieldRead (old Node.subtree) (fieldRead (old Node.right) x))"; */ /*: noteThat ROPart: "ALL x y. y : x..Node.right..Node.subtree & y ~= e --> x..Node.v <= y..Node.v"; */ /*: noteThat ROEnd: "theinv RightOrderingInv" from ROEnd, ROPart, EIsolated, ENotRight, ENoParent; */ } else { // e has both a left and a right child Node r = removeMin(e); swap(e, r); } } } }