00001
00005 package edu.mit.csail.sdg.squander.examples.bst;
00006
00007 import java.text.MessageFormat;
00008 import java.util.HashSet;
00009
00010 import edu.mit.csail.sdg.annotations.Case;
00011 import edu.mit.csail.sdg.annotations.Ensures;
00012 import edu.mit.csail.sdg.annotations.Invariant;
00013 import edu.mit.csail.sdg.annotations.Modifies;
00014 import edu.mit.csail.sdg.annotations.Nullable;
00015 import edu.mit.csail.sdg.annotations.Pure;
00016 import edu.mit.csail.sdg.annotations.Requires;
00017 import edu.mit.csail.sdg.annotations.Returns;
00018 import edu.mit.csail.sdg.annotations.SpecField;
00019 import edu.mit.csail.sdg.annotations.Specification;
00020 import edu.mit.csail.sdg.squander.Squander;
00021 import edu.mit.csail.sdg.squander.annotations.Fresh;
00022 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00023 import edu.mit.csail.sdg.squander.annotations.Options;
00024
00033 @SpecField("nodes : set Node | this.nodes = this.root.*(left+right) - null")
00034 @Invariant("this.root.parent in null")
00035
00036 public final class BinarySearchTree {
00037
00038 @Invariant( {
00039 "this.left != null => this.left.parent = this",
00040 "this.right != null => this.right.parent = this",
00041 "this.parent != null => this in this.parent.(left + right)",
00042 "this !in this.^parent",
00043 "all x : this.left.*(left + right) - null | x.key < this.key",
00044 "all x : this.right.*(left + right) - null | x.key > this.key"
00045 })
00046 public final static class Node {
00047 Node left;
00048 Node right;
00049 Node parent;
00050 int key;
00051
00052 Node() {}
00053
00054 public Node(int key) { this.key = key; }
00055
00056 public Node getLeft() { return left; }
00057 public Node getRight() { return right; }
00058 public Node getParent() { return parent; }
00059 public int getKey() { return key; }
00060
00061 public int size() {
00062 return 1 + (left != null ? left.size() : 0) + (right != null ? right.size() : 0);
00063 }
00064
00065 boolean repOk(HashSet<Node> visited) {
00066 if (!visited.add(this))
00067 return false;
00068 if (left != null) {
00069 if (left.key >= key) return false;
00070 if (left.parent != this) return false;
00071 if (!left.repOk(visited)) return false;
00072 }
00073 if (right != null) {
00074 if (right.key <= key) return false;
00075 if (right.parent != this) return false;
00076 if (!right.repOk(visited)) return false;
00077 }
00078 return true;
00079 }
00080
00081 @Override
00082 public String toString() {
00083 return MessageFormat.format("{0}", key);
00084 }
00085 }
00086
00087 @Nullable
00088 private Node root;
00089
00090 @Ensures("no this.nodes")
00091 public BinarySearchTree() {
00092 root = null;
00093 }
00094
00095 public Node getRoot() { return root; }
00096 public void setRoot(Node root) { this.root = root; }
00097
00098 public int size() {
00099 if (root == null)
00100 return 0;
00101 return root.size();
00102 }
00103
00104 public boolean repOk() {
00105 if (root == null)
00106 return true;
00107 return root.repOk(new HashSet<Node>());
00108 }
00109
00110 @Requires( {"z.key !in this.nodes.key",
00111 "z.(parent + left + right) = null",
00112 "no root.z" })
00113 @Ensures("this.nodes = @old(this.nodes + z)")
00114 @Modifies("Node.left, Node.right, Node.parent, this.root, this.nodes")
00115 public BinarySearchTree insert(Node z) {
00116 if (root == null) {
00117 root = z;
00118 root.parent = null;
00119 return this;
00120 }
00121 Node parent = null;
00122 Node current = root;
00123 while (true) {
00124 parent = current;
00125 if (z.key > current.key) {
00126 current = current.right;
00127 if (current == null) {
00128 parent.right = z;
00129 z.parent = parent;
00130 break;
00131 }
00132 } else {
00133 current = current.left;
00134 if (current == null) {
00135 parent.left = z;
00136 z.parent = parent;
00137 break;
00138 }
00139 }
00140 }
00141 return this;
00142 }
00143
00144 @Returns("keyToFind in this.nodes.key ? {n in this.nodes | n.key == keyToFind} : null")
00145 @Pure
00146 public Node findNode(int keyToFind) {
00147 Node currNode = root;
00148 while (currNode != null) {
00149 if (currNode.key == keyToFind)
00150 return currNode;
00151 else if (keyToFind > currNode.key)
00152 currNode = currNode.right;
00153 else
00154 currNode = currNode.left;
00155 }
00156 return null;
00157 }
00158
00159 @Returns("some this.nodes ? {k in this.nodes.key | no y in this.nodes | y.key < k} : -1")
00160 @Pure
00161 public int min() {
00162 if (root == null)
00163 return -1;
00164 Node n = root;
00165 while (n.left != null)
00166 n = n.left;
00167 return n.key;
00168 }
00169
00170 @Returns("some this.nodes ? {k in this.nodes.key | no y in this.nodes | y.key > k} : -1")
00171 @Pure
00172 public int max() {
00173 if (root == null)
00174 return -1;
00175 Node n = root;
00176 while (n.right != null)
00177 n = n.right;
00178 return n.key;
00179 }
00180
00181 @Returns("some this.nodes ? {k in this.nodes.key | no y in this.nodes | y.key > k} : -1")
00182 public int max_squander() {
00183 return Squander.exe(this);
00184 }
00185
00186 @Returns("some this.nodes ? {k in this.nodes.key | no y in this.nodes | y.key < k} : -1")
00187 public int min_squander() {
00188 return Squander.exe(this);
00189 }
00190
00191 @Returns("keyToFind in this.nodes.key ? {n in this.nodes | n.key == keyToFind} : null")
00192 public Node findNode_squander(int keyToFind) {
00193 return Squander.exe(this, new Class<?>[] {int.class}, new Object[] {keyToFind});
00194 }
00195
00196 @Requires("nodeToRemove in this.nodes")
00197 @Ensures("this.nodes = @old(this.nodes) - nodeToRemove")
00198 @Modifies("this.nodes, this.root, Node.left, Node.right, Node.parent")
00199 public void removeNode_squander(Node nodeToRemove) {
00200 Squander.exe(this, new Class<?>[] {Node.class}, new Object[] {nodeToRemove});
00201 }
00202
00203 @Specification({
00204 @Case(requires = {"this.root != null",
00205 "z.key !in this.nodes.key",
00206 "z.(left + right + parent) = null"},
00207 ensures = "this.nodes = @old(this.nodes + z)",
00208 modifies = "Node.left, Node.right, Node.parent, this.root, this.nodes"),
00209 @Case(requires = {"this.root == null",
00210 "z.(left + right + parent) = null"},
00211 ensures = "this.root = z",
00212 modifies = "this.root, this.nodes")
00213 })
00214 public void insertNode_squander(Node z) {
00215 Squander.exe(this, new Class<?>[] {Node.class}, new Object[] {z});
00216 }
00217
00218 @Requires( {"k !in this.nodes.key"})
00219 @Ensures("@old(this.nodes) in this.nodes && @old(this.nodes.key) in this.nodes.key && k in this.nodes.key")
00220 @Modifies("Node.left, Node.right, Node.parent, Node.key, this.root, this.nodes")
00221 @Fresh({@FreshObjects(cls=Node.class, num=1)})
00222 public void insertKey_squander(int k) {
00223 Squander.exe(this, new Class<?>[] {int.class}, new Object[] {k});
00224 }
00225
00226 @Ensures("return[int] = this.nodes && return.length = #this.nodes")
00227 @Modifies({"return.length", "return.elems"})
00228 @Fresh({@FreshObjects(cls = Node[].class, num = 1)})
00229 public Node[] getAllNodes_squander() {
00230 return Squander.exe(this);
00231 }
00232
00233 @Pure
00234 @Override
00235 public String toString() {
00236 if (root == null)
00237 return "null";
00238 return printNode(root);
00239 }
00240
00241 private String printNode(Node node) {
00242 if (node == null)
00243 return "null";
00244 return String.format("{%d(left=%s, right=%s)}", node.key, printNode(node.left), printNode(node.right));
00245 }
00246
00247
00248 private static final int NUM_NODES = 20;
00249
00250 @Fresh({
00251 @FreshObjects(cls=BinarySearchTree.class, num=1),
00252 @FreshObjects(cls=Node.class, num=NUM_NODES)
00253 })
00254 @Ensures({"#this.nodes = " + NUM_NODES})
00255 @Modifies("this.nodes, this.root, Node.left, Node.right, Node.key, Node.parent")
00256 @Options(solveAll = true)
00257 public void genBST() {
00258 Squander.exe(this);
00259 }
00260
00261 public static void main(String[] args) {
00262 BinarySearchTree bst = new BinarySearchTree();
00263 Node node1 = new Node(3);
00264 Node node2 = new Node(-4);
00265 Node node3 = new Node(-2);
00266 Node node4 = new Node(2);
00267 bst.insert(node1).insert(node2).insert(node3).insert(node4);
00268 Node node5 = new Node(6);
00269 bst.insertNode_squander(node5);
00270
00271
00272
00273
00274
00275
00276 }
00277
00278
00279
00280
00283
00284
00285
00286
00287
00288
00289
00290
00291
00292
00293
00294
00295
00296
00297
00298
00299
00300
00301
00302
00303
00304
00305
00306
00307
00308
00309
00310
00311
00312
00313
00314
00315
00316
00317
00318
00319
00320
00321
00322
00323
00329
00330
00331
00332
00333 }