00001
00005 package edu.mit.csail.sdg.squander.examples.setpoly;
00006
00007 import java.util.Set;
00008
00009 import edu.mit.csail.sdg.annotations.Ensures;
00010 import edu.mit.csail.sdg.annotations.Modifies;
00011 import edu.mit.csail.sdg.annotations.SpecField;
00012 import edu.mit.csail.sdg.squander.Squander;
00013 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00014
00015
00016 @SpecField("elems: set int")
00017 public class IntSet {
00018
00019 public IntSet() { init(); }
00020
00021 @Ensures("no this.elems")
00022 private void init() { Squander.exe(this); }
00023
00024 @Ensures("return = e !in @old(this.elems) && this.elems = @old(this.elems) @+ e")
00025 @Modifies("this.elems")
00026 public boolean add(int e) { return Squander.exe(this, e); }
00027
00028 @Ensures("return = e in this.elems")
00029 public boolean contains(int e) { return Squander.exe(this, e); }
00030
00031 @Ensures("return = s2.elems in this.elems")
00032 public boolean containsAll(IntSet s2) { return Squander.exe(this, s2); }
00033
00034 @Ensures("return = e in @old(this.elems) && this.elems = @old(this.elems) @- e")
00035 @Modifies("this.elems")
00036 public boolean remove(int e) { return Squander.exe(this, e); }
00037
00038 @Ensures("return.elts = this.elems")
00039 @FreshObjects(cls=Set.class, typeParams={Integer.class}, num=1)
00040 @Modifies("return.elts")
00041 public Set<Integer> nodes() { return Squander.exe(this); }
00042
00043 public static void main(String[] args) {
00044 IntSet s1 = new SetIntSet();
00045 IntSet s2 = new SetIntSet();
00046 s1.add(2);
00047 s1.add(3);
00048 s1.add(4);
00049 s2.add(3);
00050 s2.add(2);
00051 System.out.println(s1.containsAll(s2));
00052 s1.remove(2);
00053 System.out.println(s1.containsAll(s2));
00054 }
00055
00056 public static void main2(String[] args) {
00057 IntSet ss =
00058
00059 new SetIntSet();
00060
00061 ss.add(2);
00062 ss.remove(3);
00063 ss.add(3);
00064
00065 ss.add(2);
00066 ss.add(5);
00067 ss.add(7);
00068
00069 System.out.println(ss.nodes());
00070 System.out.println(ss);
00071 }
00072 }