00001
00005 package edu.mit.csail.sdg.squander.examples.bst;
00006
00007 import edu.mit.csail.sdg.annotations.Invariant;
00008 import edu.mit.csail.sdg.squander.annotations.Options;
00009 import edu.mit.csail.sdg.squander.log.Log.Level;
00010 import edu.mit.csail.sdg.squander.options.GlobalOptions;
00011
00021 @Invariant("all n: this.nodes | (#n.left.^(left+right) - #n.right.^(left+right)) in this.diff[int]")
00022 public class BalancedBST extends BST_noParent {
00023
00024 @SuppressWarnings("unused")
00025 private final int[] diff = new int[] {-1, 0, 1};
00026
00027 @Override
00028 public boolean repOk() {
00029 boolean b = super.repOk();
00030 if (!b)
00031 return false;
00032 return check(root);
00033 }
00034 private boolean check(Node n) {
00035 if (n == null)
00036 return true;
00037 int lhsSize = 0;
00038 if (n.left != null)
00039 lhsSize = n.left.size();
00040 int rhsSize = 0;
00041 if (n.right != null)
00042 rhsSize = n.right.size();
00043 if (Math.abs(lhsSize - rhsSize) > 1)
00044 return false;
00045 if (!check(n.left))
00046 return false;
00047 if (!check(n.right))
00048 return false;
00049 return true;
00050 }
00051
00052 @Options(ensureAllInts = true)
00053 @Override
00054 public void insertKey_squander(int k) {
00055 super.insertKey_squander(k);
00056 }
00057
00058 @Options(ensureAllInts = true)
00059 @Override
00060 public void insertNode_slow_squander(Node z) {
00061 super.insertNode_slow_squander(z);
00062 }
00063
00064 @Options(ensureAllInts = true)
00065 @Override
00066 public void removeNode_squander(Node nodeToRemove) {
00067 super.removeNode_squander(nodeToRemove);
00068 }
00069
00070 public static void main(String[] args) {
00071 GlobalOptions.INSTANCE.log_level = Level.NONE;
00072
00073 BST_noParent bst = new BalancedBST();
00074 bst.insertKey_squander(4);
00075 System.out.println(bst);
00076 assert bst.repOk();
00077
00078 bst.insertKey_squander(6);
00079 System.out.println(bst);
00080 assert bst.repOk();
00081
00082 bst.insertKey_squander(5);
00083 System.out.println(bst);
00084 assert bst.repOk();
00085
00086 bst.insertKey_squander(7);
00087 System.out.println(bst);
00088 assert bst.repOk();
00089
00090 bst.insertKey_squander(1);
00091 System.out.println(bst);
00092 assert bst.repOk();
00093
00094 bst.insertKey_squander(8);
00095 System.out.println(bst);
00096 assert bst.repOk();
00097
00098 bst.removeNode_squander(bst.findNode(5));
00099 System.out.println(bst);
00100 assert bst.repOk();
00101
00102 bst.removeNode_squander(bst.findNode(1));
00103 System.out.println(bst);
00104 assert bst.repOk();
00105
00106 bst.removeNode_squander(bst.findNode(7));
00107 System.out.println(bst);
00108 assert bst.repOk();
00109
00110 bst.removeNode_squander(bst.findNode(4));
00111 System.out.println(bst);
00112 assert bst.repOk();
00113
00114 bst.removeNode_squander(bst.findNode(6));
00115 System.out.println(bst);
00116 assert bst.repOk();
00117
00118 bst.removeNode_squander(bst.findNode(8));
00119 System.out.println(bst);
00120 assert bst.repOk();
00121 }
00122
00123 }