00001
00005 package edu.mit.csail.sdg.squander.examples.rbt;
00006
00007 import edu.mit.csail.sdg.annotations.Case;
00008 import edu.mit.csail.sdg.annotations.Effects;
00009 import edu.mit.csail.sdg.annotations.Ensures;
00010 import edu.mit.csail.sdg.annotations.Invariant;
00011 import edu.mit.csail.sdg.annotations.Modifies;
00012 import edu.mit.csail.sdg.annotations.Nullable;
00013 import edu.mit.csail.sdg.annotations.Pure;
00014 import edu.mit.csail.sdg.annotations.Requires;
00015 import edu.mit.csail.sdg.annotations.Returns;
00016 import edu.mit.csail.sdg.annotations.SpecField;
00017 import edu.mit.csail.sdg.annotations.Specification;
00018 import edu.mit.csail.sdg.annotations.Throws;
00019 import edu.mit.csail.sdg.annotations.Case.Type;
00020 import edu.mit.csail.sdg.squander.Squander;
00021
00034 @SpecField("nodes : set Node | this.nodes = this.root.*(left+right) - null")
00035 public final class RedBlackTree {
00036
00037 static final boolean BLACK = true;
00038 static final boolean RED = false;
00039
00040 @Invariant( {
00041 "this.root.parent in null",
00042 "this.root != null => one root.(this.root)"})
00043 @Nullable
00044 Node root;
00045
00049 @Ensures("no this.nodes")
00050 RedBlackTree() {
00051 }
00052
00056 @Ensures("no this.nodes")
00057 @Modifies("this.root")
00058 void clear() {
00059 Squander.exe(this);
00060 }
00061
00065 @Ensures("return - null = this.nodes & (Node@key.k)")
00066 @Pure
00067 Node search(int k) {
00068 return Squander.exe(this, k);
00069 }
00070
00075 @Ensures("return - null =" +
00076 "{n : this.nodes | n.key >= k && (no m in this.nodes | m.key >= k && m.key < n.key)}")
00077 @Pure
00078 Node searchGTE(int k) {
00079 return Squander.exe(this, new Class[] { int.class }, new Integer[] { k });
00080 }
00081
00087 @Ensures( { "(some node in this.nodes | node.key <= k) => return != null",
00088 "return != null => return.key <= k",
00089 "return != null => (no node in this.nodes | node.key <= k && node.key > return.key)",
00090 "return in this.nodes + null" })
00091 @Pure
00092 Node searchLTE(int k) {
00093 return Squander.exe(this, new Class[] { int.class }, new Integer[] { k });
00094 }
00095
00101 @Specification( {
00102 @Case(requires = { "(some x:this.nodes | x.key < node.key)", "node in this.nodes" },
00103 ensures = {
00104 "return in {x in this.nodes | x.key < node.key}",
00105 "no {x : this.nodes | x.key < node.key && x.key > return.key}" }),
00106 @Case(requires = { "no x in this.nodes | x.key < node.key", "node in this.nodes" }, ensures = "return = null"),
00107 @Case(requires = "node = null", ensures = "throw in NullPointerException", type = Type.EXCEPTIONAL) })
00108 @Pure
00109 Node predecessor(Node node) {
00110 return Squander.exe(this, new Class[] { Node.class }, new Node[] { node });
00111 }
00112
00117 @Requires("node in this.nodes")
00118 @Ensures( {
00119 "(some x:this.nodes | x.key > node.key) => return != null",
00120 "return != null => return.key > node.key && (no x:this.nodes | x.key > node.key && x.key < return.key)",
00121 "return in this.nodes + null"
00122 })
00123 @Throws("NullPointerException : node = null")
00124 @Pure
00125 Node successor(Node node) {
00126 return Squander.exe(this, new Class[] { Node.class }, new Node[] { node });
00127 }
00128
00132 @Returns("some this.nodes ? {x in this.nodes | no y in this.nodes | y.key < x.key} : null")
00133 @Pure
00134 Node minAll() {
00135 return Squander.exe(this);
00136 }
00137
00141 @Returns("some this.nodes ? {x in this.nodes | no y in this.nodes | y.key > x.key} : null")
00142 @Pure
00143 Node maxAll() {
00144 return Squander.exe(this);
00145 }
00146
00151 @Requires( {"no tree : IntTree | tree.root = n",
00152 "o in this.nodes",
00153 "n.(left + right + parent) = null",
00154 "o = o.parent.left => n.key < o.parent.key",
00155 "o = o.parent.right => n.key > o.parent.key",
00156 "o.left != null => n.key > o.left.key",
00157 "o.right != null => n.key < o.right.key", "o != n" })
00158 @Ensures( { "this.nodes = @old(this.nodes) - o + n",
00159 "o.parent + o.left + o.right = null" })
00160 @Modifies("Node.left, Node.right, Node.color, Node.parent, this.root, this.nodes")
00161 void replace(Node o, Node n) {
00162 Squander.exe(this, new Class[] { Node.class, Node.class }, new Node[] { o, n });
00163 }
00164
00169 @Requires( {"z.key !in this.nodes.key",
00170 "z.(parent + left + right) = null",
00171 "no root.z" })
00172 @Ensures("this.nodes = @old(this.nodes + z)")
00173 @Modifies("Node.left, Node.right, Node.color, Node.parent, this.root, this.nodes")
00174 void insert(Node z) {
00175 Squander.exe(this, new Class[] { Node.class }, new Node[] { z });
00176 }
00177
00182 @Requires("z in this.nodes")
00183 @Effects("this.nodes = @old(this.nodes - z)")
00184 @Modifies("this.nodes, this.root, Node.left, Node.right, Node.color, Node.parent")
00185 void delete(Node z) {
00186 Squander.exe(this, new Class[] { Node.class }, new Node[] { z });
00187 }
00188
00189 @Invariant( {
00190 "this.left != null => this.left.parent = this",
00191 "this.right != null => this.right.parent = this",
00192 "this.parent != null => this in this.parent.(left + right)",
00193 "this !in this.^parent",
00194 "all x : this.left.^(left + right) + this.left - null | x.key < this.key",
00195 "all x : this.right.^(left + right) + this.right - null | x.key > this.key",
00196 " this.color = false && this.parent != null => this.parent.color = true"})
00197 public static class Node {
00198 public final Node parent, left, right;
00199 public final boolean color;
00200 public final int key;
00201
00202 Node(int key) {
00203 this.parent = this.left = this.right = null;
00204 this.color = BLACK;
00205 this.key = key;
00206 }
00207 }
00208 }