00001
00005 package edu.mit.csail.sdg.squander.examples.javacol;
00006
00007 import java.util.HashMap;
00008 import java.util.HashSet;
00009 import java.util.LinkedList;
00010 import java.util.List;
00011 import java.util.Map;
00012 import java.util.Set;
00013
00014 import edu.mit.csail.sdg.annotations.Ensures;
00015 import edu.mit.csail.sdg.annotations.Modifies;
00016 import edu.mit.csail.sdg.squander.Squander;
00017 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00018
00019 class Str {
00020 final String msg;
00021 public Str(String msg) { this.msg = msg; }
00022 }
00023
00024 public class TypeParamsEx {
00025
00026 Map<Str, Integer> map = new HashMap<Str, Integer>();
00027 List<String> list = new LinkedList<String>();
00028 Set<String> sss = new HashSet<String>();
00029 Map<Integer, Set<String>> ms = new HashMap<Integer, Set<String>>();
00030
00031 public TypeParamsEx() {
00032 init();
00033 }
00034
00035 private void init() {
00036 map.put(new Str("str1"), 1);
00037 map.put(new Str("str2"), 2);
00038 map.put(new Str("str3"), 3);
00039
00040 list.add("str1");
00041 list.add("str4");
00042
00043 Set<String> s1 = new HashSet<String>();
00044 s1.add("1");
00045 s1.add("I");
00046 ms.put(1, s1);
00047 Set<String> s2 = new HashSet<String>();
00048 s2.add("2");
00049 s2.add("II");
00050 ms.put(2, s2);
00051 Set<String> s5 = new HashSet<String>();
00052 s5.add("5");
00053 s5.add("V");
00054 ms.put(5, s5);
00055 }
00056
00057 @Ensures("key in this.ms.elts[return].elts")
00058 public int findInt(String key) {
00059 return Squander.exe(this, key);
00060 }
00061
00062 @Ensures("return.elts = (this.map.keys.msg & this.list.elts[int])")
00063 @Modifies("return.elts")
00064 @FreshObjects(cls=Set.class, typeParams={String.class}, num=1)
00065 public Set<String> common() {
00066 return Squander.exe(this);
00067 }
00068
00069 @Ensures("this.sss.elts = (this.map.keys.msg & this.list.elts[int])")
00070 @Modifies("this.sss.elts")
00071 public void common2() {
00072 Squander.exe(this);
00073 }
00074
00075 @Ensures("return = m.elts[s]")
00076 public static Integer get(Map<String, Integer> m, String s) {
00077 return Squander.exe(null, m, s);
00078 }
00079
00080 public static void main1(String[] args) {
00081 Map<String, Integer> m = new HashMap<String, Integer>();
00082 m.put("111", 1);
00083 m.put("222", 2);
00084 m.put("555", 5);
00085 System.out.println(get(m, "111"));
00086 }
00087
00088 public static void main(String[] args) {
00089 Set<String> set = new TypeParamsEx().common();
00090 System.out.println(set);
00091 }
00092
00093 public static void main3(String[] args) {
00094 TypeParamsEx tp = new TypeParamsEx();
00095 tp.common2();
00096 System.out.println(tp.sss);
00097 }
00098
00099 public static void main4(String[] args) {
00100
00101 System.out.println(new TypeParamsEx().findInt("V"));
00102 }
00103 }