add bst oop

Author: daejunpark

verification/Makefile

@@ -21,6 +21,9 @@ prove:
 	krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst/string_find_spec.k    bst/find.js 
 	krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst/string_insert_spec.k  bst/insert.js 
 	krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst/string_delete_spec.k  bst/delete.js 
+	@echo "BST OOP String"
+	krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst-oop/bst_find_spec.k   bst-oop/bst.js 
+	krun -d patterns/tree_string --smt_prelude $(K_Z3)/string.smt2 --prove bst-oop/bst_insert_spec.k bst-oop/bst.js 
 	@echo "BST Float"
 	krun -d patterns/tree_float  --smt_prelude $(K_Z3)/float.smt2  --prove bst/float_find_spec.k     bst/find.js 
 	krun -d patterns/tree_float  --smt_prelude $(K_Z3)/float.smt2  --prove bst/float_insert_spec.k   bst/insert.js 

verification/bst-oop/bst.js

@@ -0,0 +1,81 @@
+// Binary Search Tree
+
+BST = function () {
+  this.root = null;
+};
+
+BST.prototype.insert = function (v) {
+  if (this.root == null) {
+    this.root = new BST.Node(v);
+  } else {
+    this.root.insert(v);
+  }
+};
+
+BST.prototype.find = function (v) {
+  if (this.root == null) {
+    return false;
+  } else {
+    return this.root.find(v);
+  }
+};
+
+// Binary Search Tree Node
+
+BST.Node = function (v) {
+  this.value = v;
+  this.left  = null;
+  this.right = null;
+};
+
+BST.Node.prototype.insert = function (v) {
+  if (v < this.value) {
+    if (this.left == null) {
+      this.left = new BST.Node(v);
+    } else {
+      this.left.insert(v);
+    }
+  } else if (v > this.value) {
+    if (this.right == null) {
+      this.right = new BST.Node(v);
+    } else {
+      this.right.insert(v);
+    }
+  }
+};
+
+BST.Node.prototype.find = function (v) {
+  if (v < this.value) {
+    if (this.left == null) {
+      return false;
+    } else {
+      return this.left.find(v);
+    }
+  } else if (v > this.value) {
+    if (this.right == null) {
+      return false;
+    } else {
+      return this.right.find(v);
+    }
+  } else {
+    return true;
+  }
+};
+
+
+
+
+
+
+// function Main() {
+//   var t = new BST();
+//   t.insert(2);
+//   t.insert(1);
+//   t.insert(3);
+//   console.log(t);
+//   console.log(t.find(1));
+//   console.log(t.find(2));
+//   console.log(t.find(3));
+//   console.log(t.find(4));
+// }
+// Main();

verification/bst-oop/bst_find_spec.k

@@ -0,0 +1,32 @@
+require "../../js.k"
+
+module BST-SPEC
+
+imports JS
+
+rule
+  <envs>
+    ...
+    ENVS:Bag
+    (.Bag => ?_:Bag)
+    ...
+  </envs>
+  <objs>
+    ...
+    OBJS:Bag
+    string_tree(O)(T:StringTree)(@o(8))
+    (.Bag => ?_:Bag)
+    ...
+  </objs>
+  <k>
+    Call(@o(11), O:Oid, @Cons(V:String, @Nil))
+  =>
+    V inStringSet string_tree_keys(T)
+    ...
+  </k>
+  requires string_bst(T)
+
+// @o(8)  : BST.Node.prototype
+// @o(11) : BST.Node.prototype.find
+
+endmodule

verification/bst-oop/bst_insert_spec.k

@@ -0,0 +1,37 @@
+require "../../js.k"
+
+module BST-SPEC
+
+imports JS
+
+rule
+  <envs>
+    ...
+    ENVS:Bag
+    (.Bag => ?_:Bag)
+    ...
+  </envs>
+  <objs>
+    ...
+    OBJS:Bag
+  (
+    string_tree(O1)(T1:StringTree)(@o(8))
+  =>
+    string_tree(O1)(?T2:StringTree)(@o(8))
+    ?_:Bag
+  )
+    ...
+  </objs>
+  <k>
+    Call(@o(9), O1:Oid, @Cons(V:String, @Nil))
+  =>
+    Undefined
+    ...
+  </k>
+  requires string_bst(T1)
+  ensures string_bst(?T2) andBool string_tree_keys(?T2) ==K { V } U string_tree_keys(T1)
+
+// @o(8)  : BST.Node.prototype
+// @o(9)  : BST.Node.prototype.insert
+
+endmodule