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