00001
00005 package edu.mit.csail.sdg.squander.examples.setpoly;
00006
00007 import edu.mit.csail.sdg.annotations.Invariant;
00008 import edu.mit.csail.sdg.annotations.Modifies;
00009 import edu.mit.csail.sdg.annotations.SpecField;
00010 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00011
00012 @SpecField({
00013 "elems: set int from this.nodes | this.elems = this.nodes.key",
00014 "nodes: set Node from this.root, Node.left, Node.right | this.nodes = this.root.*(left+right) - null"
00015 })
00016 public class BstIntSet extends IntSet {
00017
00018 @Invariant( {
00019 "all x : this.left.*(left + right) - null | x.key < this.key",
00020 "all x : this.right.*(left + right) - null | x.key > this.key"
00021 })
00022 public static class Node {
00023 public int key;
00024 public Node left;
00025 public Node right;
00026
00027 public Node() { this(-1); }
00028 public Node(int key) { this.key = key; }
00029 }
00030
00031 private Node root = null;
00032
00033 @Override
00034 @Modifies("Node.key")
00035 @FreshObjects(cls = Node.class, num = 1)
00036 public boolean add(int e) {
00037 return super.add(e);
00038 }
00039
00040 @Override
00041 public String toString() {
00042 return printNode(root);
00043 }
00044
00045 private String printNode(Node n) {
00046 if (n == null) {
00047 return "-";
00048 }
00049 if (n.left == null && n.right == null)
00050 return Integer.toString(n.key);
00051 return String.format("%s (%s, %s)", n.key, printNode(n.left), printNode(n.right));
00052 }
00053
00054 }