Jennisys: (1) fixed a bug in "TryInferConditionals"; (2) added synthesized modular code

author: Aleksandar Milicevic <unknown> 2011-07-29 20:02:30 -0700
committer: Aleksandar Milicevic <unknown> 2011-07-29 20:02:30 -0700
commit: 837afdf94e5a77f27f0a4e7ab334619216d3f983 (patch)
tree: 3caf3e11b2650bfab57981f187ae47d57dbfef86 /Jennisys
parent: d1dfcbe235ef8f06e0a7c03991b1e085fde9e63e (diff)
7 files changed, 1549 insertions, 8 deletions
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 831fa0f6..103b7350 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -406,8 +406,8 @@ let rec MakeModular indent prog comp m cond heapInst =
     let newProg, newComp, newMthdLst, newHeapInst = GetModularBranch prog comp m heapInst
     let msol = Utils.MapSingleton (newComp,m) [cond, newHeapInst]
     newMthdLst |> List.fold (fun acc (c,m) -> 
-                                  acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 
-                              ) msol     
+                               acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 
+                             ) msol     
   else 
     Utils.MapSingleton (comp,m) [cond, heapInst]
 
@@ -520,12 +520,14 @@ and TryInferConditionals indent prog comp m unifs heapInst =
         else 
           true
       if verified then
-        if Options.CONFIG.verifyPartialSolutions then
-          Logger.InfoLine "VERIFIED"
-        else 
-          Logger.InfoLine "SKIPPED"
+        if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"
         let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(candCond))
-        MergeSolutions sol (AnalyzeConstructor (indent + 2) p3 c3 m3)
+        let fixedSol = sol |> Map.fold (fun acc (cc,mm) v -> 
+                                          if GetMethodName mm = GetMethodName m then
+                                            acc |> Map.add (cc,m) v
+                                          else 
+                                            acc |> Map.add (cc,mm) v) Map.empty
+        MergeSolutions fixedSol (AnalyzeConstructor (indent + 2) p3 c3 m3)
       else 
         Logger.InfoLine "NOT VERIFIED"
         wrongSol                     
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 79c273eb..28e6b931 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>
     <PlatformTarget>x86</PlatformTarget>
     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>
-    <StartArguments>examples/List3.jen /method:IntList.OneTwo /genRepr  /genMod</StartArguments>
+    <StartArguments>examples/Set.jen /method:Set.Double /genRepr  /genMod</StartArguments>
     <StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>
   </PropertyGroup>
   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_List.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_List.dfy
new file mode 100644
index 00000000..474eb9f1
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod/jennisys-synth_List.dfy
@@ -0,0 +1,202 @@
+class List<T> {
+  ghost var Repr: set<object>;
+  ghost var list: seq<T>;
+
+  var root: Node<T>;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (root == null ==> |list| == 0) &&
+    (root != null ==> list == root.list)
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (root != null ==> root.Valid())
+  }
+
+
+  method Double(p: T, q: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p, q];
+  {
+    var gensym68 := new Node<T>;
+    gensym68._synth_List_Double_gensym68(p, q);
+    this.list := [p, q];
+    this.root := gensym68;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Empty()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [];
+  {
+    this.list := [];
+    this.root := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Singleton(t: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [t];
+  {
+    var gensym69 := new Node<T>;
+    gensym69._synth_List_Singleton_gensym69(t);
+    this.list := [t];
+    this.root := gensym69;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+}
+
+class Node<T> {
+  ghost var Repr: set<object>;
+  ghost var list: seq<T>;
+
+  var data: T;
+  var next: Node<T>;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (next == null <==> list == [data] && list[0] == data) &&
+    (next != null ==> list == [data] + next.list) &&
+    (|list| > 0)
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (next != null ==> next.Valid_self()) &&
+    (next != null && next.next != null ==> next.next.Valid_self())
+  }
+
+
+  method Init(t: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [t];
+  {
+    this.data := t;
+    this.list := [t];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_List_Double_gensym68(p: T, q: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 2;
+    ensures list[0] == p;
+    ensures list[1] == q;
+  {
+    var gensym75 := new Node<T>;
+    gensym75._synth_Node__synth_List_Double_gensym68_gensym75(q);
+    this.data := p;
+    this.list := [p, q];
+    this.next := gensym75;
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_List_Singleton_gensym69(t: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == t;
+  {
+    this.data := t;
+    this.list := [t];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Double(p: T, q: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p, q];
+  {
+    var gensym73 := new Node<T>;
+    gensym73._synth_Node_Double_gensym73(q);
+    this.data := p;
+    this.list := [p, q];
+    this.next := gensym73;
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_Node_Double_gensym73(q: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == q;
+  {
+    this.data := q;
+    this.list := [q];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_Node__synth_List_Double_gensym68_gensym75(q: T)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == q;
+  {
+    this.data := q;
+    this.list := [q];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_List2.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_List2.dfy
new file mode 100644
index 00000000..46213b46
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod/jennisys-synth_List2.dfy
@@ -0,0 +1,323 @@
+class IntList {
+  ghost var Repr: set<object>;
+  ghost var list: seq<int>;
+
+  var root: IntNode;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (root == null <==> |list| == 0) &&
+    (root != null ==> list == root.list)
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (root != null ==> root.Valid())
+  }
+
+
+  method Double(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p] + [q];
+  {
+    var gensym67 := new IntNode;
+    gensym67._synth_IntList_Double_gensym67(p, q);
+    this.list := [p] + [q];
+    this.root := gensym67;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Empty()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [];
+  {
+    this.list := [];
+    this.root := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method OneTwo()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [1, 2];
+  {
+    var gensym65 := new IntNode;
+    gensym65._synth_IntList_OneTwo_gensym65();
+    this.list := [1, 2];
+    this.root := gensym65;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Singleton(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p];
+  {
+    var gensym70 := new IntNode;
+    gensym70._synth_IntList_Singleton_gensym70(p);
+    this.list := [p];
+    this.root := gensym70;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method SingletonTwo()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [2];
+  {
+    var gensym69 := new IntNode;
+    gensym69._synth_IntList_SingletonTwo_gensym69();
+    this.list := [2];
+    this.root := gensym69;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Sum(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p + q];
+  {
+    var gensym71 := new IntNode;
+    gensym71._synth_IntList_Sum_gensym71(p, q);
+    this.list := [p + q];
+    this.root := gensym71;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method TwoConsecutive(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p] + [p + 1];
+  {
+    var gensym66 := new IntNode;
+    gensym66._synth_IntList_TwoConsecutive_gensym66(p);
+    this.list := [p] + [p + 1];
+    this.root := gensym66;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+}
+
+class IntNode {
+  ghost var Repr: set<object>;
+  ghost var list: seq<int>;
+
+  var data: int;
+  var next: IntNode;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (next == null ==> list == [data] && list[0] == data) &&
+    (next != null ==> list == [data] + next.list) &&
+    (|list| > 0)
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (next != null ==> next.Valid_self()) &&
+    (next != null && next.next != null ==> next.next.Valid_self())
+  }
+
+
+  method SingletonZero()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [0];
+  {
+    this.data := 0;
+    this.list := [0];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_Double_gensym67(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p] + [q];
+  {
+    var gensym78 := new IntNode;
+    gensym78._synth_IntNode__synth_IntList_Double_gensym67_gensym78(q);
+    this.data := p;
+    this.list := [p] + [q];
+    this.next := gensym78;
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_IntList_OneTwo_gensym65()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 2;
+    ensures list[0] == 1;
+    ensures list[1] == 2;
+  {
+    var gensym75 := new IntNode;
+    gensym75._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym75();
+    this.data := 1;
+    this.list := [1, 2];
+    this.next := gensym75;
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_IntList_SingletonTwo_gensym69()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == 2;
+  {
+    this.data := 2;
+    this.list := [2];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_Singleton_gensym70(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == p;
+  {
+    this.data := p;
+    this.list := [p];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_Sum_gensym71(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == p + q;
+  {
+    this.data := p + q;
+    this.list := [p + q];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_TwoConsecutive_gensym66(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p] + [p + 1];
+  {
+    var gensym78 := new IntNode;
+    gensym78._synth_IntNode__synth_IntList_TwoConsecutive_gensym66_gensym78(p);
+    this.data := p;
+    this.list := [p] + [p + 1];
+    this.next := gensym78;
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_IntNode__synth_IntList_Double_gensym67_gensym78(q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == q;
+  {
+    this.data := q;
+    this.list := [q];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym75()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == 2;
+  {
+    this.data := 2;
+    this.list := [2];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntNode__synth_IntList_TwoConsecutive_gensym66_gensym78(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures |list| == 1;
+    ensures list[0] == p + 1;
+  {
+    this.data := p + 1;
+    this.list := [p + 1];
+    this.next := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy
new file mode 100644
index 00000000..e079b608
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod/jennisys-synth_List3.dfy
@@ -0,0 +1,393 @@
+class IntList {
+  ghost var Repr: set<object>;
+  ghost var list: seq<int>;
+
+  var root: IntNode;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (root == null ==> |list| == 0) &&
+    (root != null ==> |list| == |root.succ| + 1 && (list[0] == root.data && (forall i :: 1 <= i && i <= |root.succ| ==> root.succ[i - 1] != null && list[i] == root.succ[i - 1].data)))
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (root != null ==> root.Valid())
+  }
+
+
+  method Double(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p] + [q];
+  {
+    var gensym68 := new IntNode;
+    gensym68._synth_IntList_Double_gensym68(p, q);
+    this.list := [p] + [q];
+    this.root := gensym68;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Empty()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [];
+  {
+    this.list := [];
+    this.root := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method OneTwo()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [1, 2];
+  {
+    var gensym65 := new IntNode;
+    gensym65._synth_IntList_OneTwo_gensym65();
+    this.list := [1, 2];
+    this.root := gensym65;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Singleton(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p];
+  {
+    var gensym70 := new IntNode;
+    gensym70._synth_IntList_Singleton_gensym70(p);
+    this.list := [p];
+    this.root := gensym70;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method SingletonTwo()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [2];
+  {
+    var gensym69 := new IntNode;
+    gensym69._synth_IntList_SingletonTwo_gensym69();
+    this.list := [2];
+    this.root := gensym69;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Sum(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p + q];
+  {
+    var gensym71 := new IntNode;
+    gensym71._synth_IntList_Sum_gensym71(p, q);
+    this.list := [p + q];
+    this.root := gensym71;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method TwoConsecutive(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures list == [p] + [p + 1];
+  {
+    var gensym67 := new IntNode;
+    gensym67._synth_IntList_TwoConsecutive_gensym67(p);
+    this.list := [p] + [p + 1];
+    this.root := gensym67;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+}
+
+class IntNode {
+  ghost var Repr: set<object>;
+  ghost var succ: seq<IntNode>;
+  ghost var data: int;
+
+  var next: IntNode;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (next == null ==> |succ| == 0) &&
+    (next != null ==> succ == [next] + next.succ) &&
+    (!(null in succ))
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (next != null ==> next.Valid_self()) &&
+    (next != null && next.next != null ==> next.next.Valid_self())
+  }
+
+
+  method Init(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p;
+  {
+    this.data := p;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method InitInc(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p + 1;
+  {
+    this.data := p + 1;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Zero()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == 0;
+    ensures succ == [];
+  {
+    this.data := 0;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_Double_gensym68(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p;
+    ensures |succ| == 1;
+    ensures succ[0].data == q;
+    ensures succ[0].succ == [];
+  {
+    var gensym80 := new IntNode;
+    gensym80._synth_IntNode__synth_IntList_Double_gensym68_gensym80(q);
+    this.data := p;
+    this.next := gensym80;
+    this.succ := [gensym80];
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_IntList_OneTwo_gensym65()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == 1;
+    ensures |succ| == 1;
+    ensures succ[0].data == 2;
+    ensures succ[0].succ == [];
+  {
+    var gensym78 := new IntNode;
+    gensym78._synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78();
+    this.data := 1;
+    this.next := gensym78;
+    this.succ := [gensym78];
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_IntList_SingletonTwo_gensym69()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == 2;
+    ensures |succ| == 0;
+  {
+    this.data := 2;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_Singleton_gensym70(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p;
+    ensures |succ| == 0;
+  {
+    this.data := p;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_Sum_gensym71(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p + q;
+    ensures |succ| == 0;
+  {
+    this.data := p + q;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntList_TwoConsecutive_gensym67(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p;
+    ensures |succ| == 1;
+    ensures succ[0].data == p + 1;
+    ensures succ[0].succ == [];
+  {
+    var gensym79 := new IntNode;
+    gensym79._synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p);
+    this.data := p;
+    this.next := gensym79;
+    this.succ := [gensym79];
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method OneTwo()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == 1;
+    ensures |succ| == 1;
+    ensures succ[0] != null;
+    ensures succ[0].data == 2;
+  {
+    var gensym73 := new IntNode;
+    gensym73._synth_IntNode_OneTwo_gensym73();
+    this.data := 1;
+    this.next := gensym73;
+    this.succ := [gensym73];
+    // repr stuff
+    this.Repr := {this} + this.next.Repr;
+  }
+
+
+  method _synth_IntNode_OneTwo_gensym73()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == 2;
+    ensures |succ| == 0;
+  {
+    this.data := 2;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntNode__synth_IntList_Double_gensym68_gensym80(q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == q;
+    ensures |succ| == 0;
+  {
+    this.data := q;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntNode__synth_IntList_OneTwo_gensym65_gensym78()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == 2;
+    ensures |succ| == 0;
+  {
+    this.data := 2;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_IntNode__synth_IntList_TwoConsecutive_gensym67_gensym79(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures data == p + 1;
+    ensures |succ| == 0;
+  {
+    this.data := p + 1;
+    this.next := null;
+    this.succ := [];
+    // repr stuff
+    this.Repr := {this};
+  }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy
new file mode 100644
index 00000000..3f1e6b4b
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy
@@ -0,0 +1,233 @@
+class Number {
+  ghost var Repr: set<object>;
+  ghost var num: int;
+
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    true
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    true
+  }
+
+
+  method Double(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num == 2 * p;
+  {
+    this.num := 2 * p;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Init(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num == p;
+  {
+    this.num := p;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Sum(a: int, b: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num == a + b;
+  {
+    this.num := a + b;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Abs(a: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num in {a, -a};
+    ensures num >= 0;
+  {
+    if (a >= 0) {
+      this.num := a;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      this.num := -a;
+      // repr stuff
+      this.Repr := {this};
+    }
+  }
+
+
+  method Min4(a: int, b: int, c: int, d: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num in {a, b, c, d};
+    ensures (forall x :: x in {a, b, c, d} ==> num <= x);
+  {
+    if (a <= b && (a <= c && a <= d)) {
+      this.num := a;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      if (d <= a && (d <= b && d <= c)) {
+        this.num := d;
+        // repr stuff
+        this.Repr := {this};
+      } else {
+        if (c <= a && (c <= b && c <= d)) {
+          this.num := c;
+          // repr stuff
+          this.Repr := {this};
+        } else {
+          this.num := b;
+          // repr stuff
+          this.Repr := {this};
+        }
+      }
+    }
+  }
+
+
+  method MinSum(a: int, b: int, c: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num in {a + b, a + c, b + c};
+    ensures num <= a + b;
+    ensures num <= b + c;
+    ensures num <= a + c;
+  {
+    if (a + b <= b + c && a + b <= a + c) {
+      this.num := a + b;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      if (a + c <= a + b && a + c <= b + c) {
+        this.num := a + c;
+        // repr stuff
+        this.Repr := {this};
+      } else {
+        this.num := b + c;
+        // repr stuff
+        this.Repr := {this};
+      }
+    }
+  }
+
+
+  method Min32(a: int, b: int, c: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num in {a, b, c};
+    ensures (forall x :: x in {a, b, c} ==> num <= x);
+  {
+    if (a <= b && a <= c) {
+      this.num := a;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      if (c <= a && c <= b) {
+        this.num := c;
+        // repr stuff
+        this.Repr := {this};
+      } else {
+        this.num := b;
+        // repr stuff
+        this.Repr := {this};
+      }
+    }
+  }
+
+
+  method Min3(a: int, b: int, c: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num in {a, b, c};
+    ensures num <= a;
+    ensures num <= b;
+    ensures num <= c;
+  {
+    if (a <= b && a <= c) {
+      this.num := a;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      if (c <= a && c <= b) {
+        this.num := c;
+        // repr stuff
+        this.Repr := {this};
+      } else {
+        this.num := b;
+        // repr stuff
+        this.Repr := {this};
+      }
+    }
+  }
+
+
+  method Min22(a: int, b: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures num in {a, b};
+    ensures num <= a;
+    ensures num <= b;
+  {
+    if (a <= b) {
+      this.num := a;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      this.num := b;
+      // repr stuff
+      this.Repr := {this};
+    }
+  }
+
+
+  method Min2(a: int, b: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures a < b ==> num == a;
+    ensures a >= b ==> num == b;
+  {
+    if (a >= b ==> a == b) {
+      this.num := a;
+      // repr stuff
+      this.Repr := {this};
+    } else {
+      this.num := b;
+      // repr stuff
+      this.Repr := {this};
+    }
+  }
+
+}
+
+
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy
new file mode 100644
index 00000000..40404bfb
--- /dev/null
+++ b/Jennisys/Jennisys/examples/mod/jennisys-synth_Set.dfy
@@ -0,0 +1,388 @@
+class Set {
+  ghost var Repr: set<object>;
+  ghost var elems: set<int>;
+
+  var root: SetNode;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (root != null ==> root in Repr && root.Repr <= Repr && this !in root.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (root == null ==> elems == {}) &&
+    (root != null ==> elems == root.elems)
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (root != null ==> root.Valid())
+  }
+
+
+  method Double(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p, q};
+  {
+    var gensym67 := new SetNode;
+    gensym67._synth_Set_Double_gensym67(p, q);
+    this.elems := {p, q};
+    this.root := gensym67;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Empty()
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {};
+  {
+    this.elems := {};
+    this.root := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Singleton(t: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {t};
+  {
+    var gensym67 := new SetNode;
+    gensym67._synth_Set_Singleton_gensym67(t);
+    this.elems := {t};
+    this.root := gensym67;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+
+  method Sum(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p + q};
+  {
+    var gensym69 := new SetNode;
+    gensym69._synth_Set_Sum_gensym69(p, q);
+    this.elems := {p + q};
+    this.root := gensym69;
+    // repr stuff
+    this.Repr := {this} + this.root.Repr;
+  }
+
+}
+
+class SetNode {
+  ghost var Repr: set<object>;
+  ghost var elems: set<int>;
+
+  var data: int;
+  var left: SetNode;
+  var right: SetNode;
+
+  function Valid_repr(): bool
+    reads *;
+  {
+    this in Repr &&
+    null !in Repr &&
+    (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&
+    (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)
+  }
+
+  function Valid_self(): bool
+    reads *;
+  {
+    Valid_repr() &&
+    (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&
+    (left != null ==> (forall e :: e in left.elems ==> e < data)) &&
+    (right != null ==> (forall e :: e in right.elems ==> e > data))
+  }
+
+  function Valid(): bool
+    reads *;
+  {
+    this.Valid_self() &&
+    (left != null ==> left.Valid_self()) &&
+    (right != null ==> right.Valid_self()) &&
+    (left != null && left.left != null ==> left.left.Valid_self()) &&
+    (left != null && left.right != null ==> left.right.Valid_self()) &&
+    (right != null && right.left != null ==> right.left.Valid_self()) &&
+    (right != null && right.right != null ==> right.right.Valid_self())
+  }
+
+
+  method Double(p: int, q: int)
+    modifies this;
+    requires p != q;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p, q};
+  {
+    if (q > p) {
+      var gensym77 := new SetNode;
+      gensym77._synth_SetNode_Double_gensym77(q);
+      this.data := p;
+      this.elems := {p, q};
+      this.left := null;
+      this.right := gensym77;
+      // repr stuff
+      this.Repr := {this} + this.right.Repr;
+    } else {
+      var gensym77 := new SetNode;
+      gensym77._synth_SetNode_Double_gensym77(p);
+      this.data := q;
+      this.elems := {p, q};
+      this.left := null;
+      this.right := gensym77;
+      // repr stuff
+      this.Repr := {this} + this.right.Repr;
+    }
+  }
+
+
+  method _synth_SetNode_Double_gensym77(q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {q};
+  {
+    this.data := q;
+    this.elems := {q};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_SetNode_Triple_gensym80(r: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {r};
+  {
+    this.data := r;
+    this.elems := {r};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Triple(p: int, q: int, r: int)
+    modifies this;
+    requires p != q;
+    requires q != r;
+    requires r != p;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p, q, r};
+  {
+    if (p < q && r > q) {
+      var gensym80 := new SetNode;
+      var gensym81 := new SetNode;
+      gensym80._synth_SetNode_Triple_gensym80(r);
+      gensym81._synth_SetNode_Triple_gensym81(p);
+      this.data := q;
+      this.elems := {p, q, r};
+      this.left := gensym81;
+      this.right := gensym80;
+      // repr stuff
+      this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+    } else {
+      if (r < p && q > p) {
+        var gensym80 := new SetNode;
+        var gensym81 := new SetNode;
+        gensym80._synth_SetNode_Triple_gensym80(q);
+        gensym81._synth_SetNode_Triple_gensym81(r);
+        this.data := p;
+        this.elems := {p, q, r};
+        this.left := gensym81;
+        this.right := gensym80;
+        // repr stuff
+        this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+      } else {
+        if (p < r && q > r) {
+          var gensym80 := new SetNode;
+          var gensym81 := new SetNode;
+          gensym80._synth_SetNode_Triple_gensym80(q);
+          gensym81._synth_SetNode_Triple_gensym81(p);
+          this.data := r;
+          this.elems := {p, q, r};
+          this.left := gensym81;
+          this.right := gensym80;
+          // repr stuff
+          this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+        } else {
+          if (r < q && p > q) {
+            var gensym80 := new SetNode;
+            var gensym81 := new SetNode;
+            gensym80._synth_SetNode_Triple_gensym80(p);
+            gensym81._synth_SetNode_Triple_gensym81(r);
+            this.data := q;
+            this.elems := {p, q, r};
+            this.left := gensym81;
+            this.right := gensym80;
+            // repr stuff
+            this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+          } else {
+            if (q < r && p > r) {
+              var gensym80 := new SetNode;
+              var gensym81 := new SetNode;
+              gensym80._synth_SetNode_Triple_gensym80(p);
+              gensym81._synth_SetNode_Triple_gensym81(q);
+              this.data := r;
+              this.elems := {p, q, r};
+              this.left := gensym81;
+              this.right := gensym80;
+              // repr stuff
+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+            } else {
+              var gensym80 := new SetNode;
+              var gensym81 := new SetNode;
+              gensym80._synth_SetNode_Triple_gensym80(r);
+              gensym81._synth_SetNode_Triple_gensym81(q);
+              this.data := p;
+              this.elems := {p, q, r};
+              this.left := gensym81;
+              this.right := gensym80;
+              // repr stuff
+              this.Repr := ({this} + this.left.Repr) + this.right.Repr;
+            }
+          }
+        }
+      }
+    }
+  }
+
+
+  method _synth_SetNode_Triple_gensym81(p: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p};
+  {
+    this.data := p;
+    this.elems := {p};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method Init(t: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {t};
+  {
+    this.data := t;
+    this.elems := {t};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_SetNode__synth_Set_Double_gensym67_gensym77(q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {q};
+  {
+    this.data := q;
+    this.elems := {q};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_Set_Double_gensym67(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p, q};
+  {
+    if (q > p) {
+      var gensym77 := new SetNode;
+      gensym77._synth_SetNode__synth_Set_Double_gensym67_gensym77(q);
+      this.data := p;
+      this.elems := {p, q};
+      this.left := null;
+      this.right := gensym77;
+      // repr stuff
+      this.Repr := {this} + this.right.Repr;
+    } else {
+      if (p > q) {
+        var gensym77 := new SetNode;
+        gensym77._synth_SetNode__synth_Set_Double_gensym67_gensym77(p);
+        this.data := q;
+        this.elems := {p, q};
+        this.left := null;
+        this.right := gensym77;
+        // repr stuff
+        this.Repr := {this} + this.right.Repr;
+      } else {
+        this.data := q;
+        this.elems := {p, q};
+        this.left := null;
+        this.right := null;
+        // repr stuff
+        this.Repr := {this};
+      }
+    }
+  }
+
+
+  method _synth_Set_Singleton_gensym67(t: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {t};
+  {
+    this.data := t;
+    this.elems := {t};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+
+  method _synth_Set_Sum_gensym69(p: int, q: int)
+    modifies this;
+    ensures fresh(Repr - {this});
+    ensures Valid();
+    ensures elems == {p + q};
+  {
+    this.data := p + q;
+    this.elems := {p + q};
+    this.left := null;
+    this.right := null;
+    // repr stuff
+    this.Repr := {this};
+  }
+
+}
+
+
author	Aleksandar Milicevic <unknown>	2011-07-29 20:02:30 -0700
committer	Aleksandar Milicevic <unknown>	2011-07-29 20:02:30 -0700
commit	837afdf94e5a77f27f0a4e7ab334619216d3f983 (patch)
tree	3caf3e11b2650bfab57981f187ae47d57dbfef86 /Jennisys
parent	d1dfcbe235ef8f06e0a7c03991b1e085fde9e63e (diff)