00001 00005 package edu.mit.csail.sdg.squander.spec; 00006 00007 import java.util.LinkedHashMap; 00008 00009 import edu.mit.csail.sdg.squander.engine.ISquander; 00010 import edu.mit.csail.sdg.squander.options.GlobalOptions; 00011 import edu.mit.csail.sdg.squander.spec.Source.Rule; 00012 00013 00014 00015 00016 public class SqFunc { 00017 00018 public static interface Binary<R, A1, A2> { 00019 public R exe(A1 arg1, A2 arg2); 00020 } 00021 00022 public static class Func { 00023 private final String requires, ensures, modifies; 00024 00025 public Func(String requires, String ensures, String modifies) { 00026 this.requires = requires; 00027 this.ensures = ensures; 00028 this.modifies = modifies; 00029 } 00030 00031 public Object exe(Object... args) { 00032 LinkedHashMap<String, Class<?>> params = new LinkedHashMap<String, Class<?>>(); 00033 for (int i = 0; i < args.length; i++) 00034 params.put("@arg(" + i + ")", args[i].getClass()); 00035 MethodSpec ms = new MethodSpec(); 00036 JMethod jm = new JMethod("<anonymous>", Null.class, params, Object.class, true); 00037 NameSpace ns = NameSpace.forMethod(jm); 00038 ms.addCase(new Source(requires, ns, Rule.CLAUSE), 00039 new Source(ensures, ns, Rule.CLAUSE), 00040 new Source(modifies, ns, Rule.FRAME), false); 00041 00042 jm.setSpec(ms); 00043 ISquander sq = GlobalOptions.INSTANCE.getSquanderImpl(); 00044 return sq.magic(null, jm, args); 00045 } 00046 } 00047 00048 public static Func mkFunc(String ensures) { 00049 return mkFunc("true", ensures, ""); 00050 } 00051 00052 public static Func mkFunc(String requires, String ensures, String modifies) { 00053 return new Func(requires, ensures, modifies); 00054 } 00055 }