00001
00005 package edu.mit.csail.sdg.squander.examples.javacol;
00006
00007 import java.util.HashMap;
00008 import java.util.List;
00009 import java.util.Map;
00010 import java.util.Set;
00011
00012 import edu.mit.csail.sdg.annotations.Ensures;
00013 import edu.mit.csail.sdg.annotations.Modifies;
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.squander.Squander;
00018 import edu.mit.csail.sdg.squander.annotations.Options;
00019
00025 @SpecField("x : one java.util.Map<String, Integer>")
00026 public class Collections {
00027
00028
00029
00030
00031
00032 @Requires("idx >= 0 && idx < list.length")
00033 @Returns("list.elts[idx]")
00034 public static <E> E get(List<E> list, int idx) {
00035 return Squander.exe(null, list, idx);
00036 }
00037
00038 @Requires("idx >= 0 && idx < list.length")
00039 @Ensures("list.elts = @old(list.elts) ++ (idx -> value)")
00040 @Modifies("list.elts")
00041 public static <E> void set(List<E> list, int idx, E value) {
00042 Squander.exe(null, list, idx, value);
00043 }
00044
00045 @Ensures({
00046 "list.elts = @old(list.elts) + (@old(list.length) -> elem)",
00047 "list.length = @old(list.length) + 1"
00048 })
00049 @Modifies("list.elts, list.length")
00050 public static <E> void add(List<E> list, E elem) {
00051 Squander.exe(null, list, elem);
00052 }
00053
00054 @Ensures("some list.prev[elem] ? return = list.prev[elem] : return = null")
00055 public static <E> E prev(List<E> list, E elem) {
00056 return Squander.exe(null, list, elem);
00057 }
00058
00059 @Ensures("some list.next[elem] ? return = list.next[elem] : return = null")
00060 public static <E> E next(List<E> list, E elem) {
00061 return Squander.exe(null, list, elem);
00062 }
00063
00064 @Requires("idx >= 0 && idx < list.length")
00065 @Ensures({
00066 "return = @old(list.elts[idx])",
00067 "all i : int | (i < idx => list.elts[i] = @old(list.elts[i])) && " +
00068 "(i >= idx && i < @old(list.length) => list.elts[i] = @old(list.elts[i+1]))",
00069 "list.length = @old(list.length) - 1"
00070 })
00071 @Modifies("list.elts, list.length")
00072 @Options(ensureAllInts = false)
00073 public static <E> E remove(List<E> list, int idx) {
00074 return Squander.exe(null, list, idx);
00075 }
00076
00077
00078
00079
00080
00081 @Ensures("key in map.keys ? return = map.elts[key] : return = null")
00082 public static <K, V> V get(Map<K, V> map, K key) {
00083 return Squander.exe(null, map, key);
00084 }
00085
00086 @Ensures({
00087 "map.elts = @old(map.elts) ++ (key -> value)",
00088 "key in @old(map.keys) ? return = @old(map.elts[key]) : return = null"
00089 })
00090 @Modifies("map.elts")
00091 public static <K, V> V put(Map<K, V> map, K key, V value) {
00092 return Squander.exe(null, map, key, value);
00093 }
00094
00095 @Ensures({
00096 "map.elts = @old(map.elts) - (key -> Object)",
00097 "key in @old(map.keys) ? return = @old(map.elts[key]) : return = null"
00098 })
00099 @Modifies("map.elts")
00100 public static <K, V> V removeKey(Map<K, V> map, K key) {
00101 return Squander.exe(null, map, key);
00102 }
00103
00104
00105
00106
00107
00108 @Returns("key in s.elts")
00109 public static <E> boolean contains(Set<E> s, E key) {
00110 return Squander.exe(null, s, key);
00111 }
00112
00113 @Ensures({
00114 "s.elts = @old(s.elts) + key",
00115 "key in @old(s.elts) ? return = false : return = true"
00116 })
00117 @Modifies("s.elts")
00118 public static <E> boolean add(Set<E> s, E key) {
00119 return Squander.exe(null, s, key);
00120 }
00121
00122 @Ensures({
00123 "s.elts = @old(s.elts) - key",
00124 "key in @old(s.elts) ? return = true : return = false"
00125 })
00126 @Modifies("s.elts")
00127 public static <E> boolean remove(Set<E> s, E key) {
00128 return Squander.exe(null, s, key);
00129 }
00130
00131 @Returns("#m<String, Integer>.elts")
00132 private int f(Map<String, Integer> m) {
00133 return Squander.exe(this, m);
00134 }
00135
00136 public static void main(String[] args) {
00137 Map<String, Integer> m = new HashMap<String, Integer>();
00138 System.out.println(new Collections().f(m));
00139 }
00140
00141 }