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