Jennisys:

   - small fixes to the modular synthesis

8 files changed, 268 insertions, 254 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index ccc1e4ab..42add00c 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -287,86 +287,69 @@ let GetHeapExpr prog mthd heapInst =
                           objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

                       ) prepostExpr

 

-let FindExisting indent comp m cond =

-  if not Options.CONFIG.genMod then

-    None

-  else 

-    let idt = Indent indent

-    match TryFindAMatch m (GetMembers comp |> FilterMethodMembers) with

-    | Some(m',unifs) -> 

-        Logger.InfoLine (idt + "    - substitution method found:")

-        Logger.InfoLine (PrintMethodSignFull (indent+6) comp m')

-        let args = ApplyMethodUnifs m' unifs

-        let delegateCall = MethodCall(ThisLiteral, GetMethodName m', args)

-        let obj = { name = "this"; objType = GetClassType comp }

-        let var = Var("", None)

-        let body = [(obj,var), delegateCall]

-        let hInst = { assignments = body; 

-                      methodArgs  = Map.empty; 

-                      globals     = Map.empty }

-        Some(Map.empty |> Map.add (comp,m) [cond, hInst]

-                       |> Map.add (comp,m') [])

-    | None -> None

+// use the orginal method, not the one with an extra precondition

+let FixSolution origMeth sol =

+  sol |> Map.fold (fun acc (cc,mm) v -> 

+                      if GetMethodName mm = GetMethodName origMeth then

+                        acc |> Map.add (cc,origMeth) v

+                      else 

+                        acc |> Map.add (cc,mm) v) Map.empty

 

 //  ============================================================================

 /// Attempts to synthesize the initialization code for the given constructor "m"

 ///

 /// Returns a (heap,env,ctx) tuple

 //  ============================================================================                           

-let rec AnalyzeConstructor indent prog comp m =

+let rec AnalyzeConstructor indent prog comp m callGraph =

   let idt = Indent indent

   Logger.InfoLine (idt + "[*] Analyzing constructor")

   Logger.InfoLine (idt + "------------------------------------------")

   Logger.InfoLine (PrintMethodSignFull (indent + 4) comp m)

   Logger.InfoLine (idt + "------------------------------------------")

-  let methodName = GetMethodName m

-  let pre,post = GetMethodPrePost m

-  // generate Dafny code for analysis first

-  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) false

-  Logger.Info     (idt + "    - searching for an instance      ...")

-  let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))  

-  if models.Count = 0 then

-    // no models means that the "assert false" was verified, which means that the spec is inconsistent

-    Logger.WarnLine (idt + " !!! SPEC IS INCONSISTENT !!!")

-    Map.empty

-  else 

-    if models.Count > 1 then 

-      Logger.WarnLine " FAILED "

-      failwith "internal error (more than one model for a single constructor analysis)"

-    Logger.InfoLine " OK "

-    let model = models.[0]

-    let hModel = ReadFieldValuesFromModel model prog comp m

-    let heapInst = ResolveModel hModel

-    let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList

-    let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

+  match TryFindExistingAndConvertToSolution indent comp m TrueLiteral callGraph with

+  | Some(sol) -> sol

+  | None -> 

+      let methodName = GetMethodName m

+      let pre,post = GetMethodPrePost m

+      // generate Dafny code for analysis first

+      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) false

+      Logger.Info     (idt + "    - searching for an instance      ...")

+      let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))  

+      if models.Count = 0 then

+        // no models means that the "assert false" was verified, which means that the spec is inconsistent

+        Logger.WarnLine (idt + " !!! SPEC IS INCONSISTENT !!!")

+        Map.empty

+      else 

+        if models.Count > 1 then 

+          Logger.WarnLine " FAILED "

+          failwith "internal error (more than one model for a single constructor analysis)"

+        Logger.InfoLine " OK "

+        let model = models.[0]

+        let hModel = ReadFieldValuesFromModel model prog comp m

+        let heapInst = ResolveModel hModel

+        let unifs = GetUnificationsForMethod indent comp m heapInst |> Map.toList

+        let heapInst = ApplyUnifications indent prog comp m unifs heapInst true

         

-    // split into method calls

-    let sol = MakeModular indent prog comp m TrueLiteral heapInst

+        // split into method calls

+        let sol = MakeModular indent prog comp m TrueLiteral heapInst callGraph |> FixSolution m

 

-    if Options.CONFIG.verifySolutions then

-      Logger.InfoLine (idt + "    - verifying synthesized solution ... ")

-      let verified = VerifySolution prog sol Options.CONFIG.genRepr

-      Logger.Info (idt + "    ")

-      if verified then

-        Logger.InfoLine "~~~ VERIFIED ~~~"

-        sol

-      else 

-        Logger.InfoLine "!!! NOT VERIFIED !!!"

-        if Options.CONFIG.inferConditionals then

-          Logger.InfoLine (idt + "    Strengthening the pre-condition")

-          TryInferConditionals (indent + 4) prog comp m unifs heapInst

+        if Options.CONFIG.verifySolutions then

+          Logger.InfoLine (idt + "    - verifying synthesized solution ... ")

+          let verified = VerifySolution prog sol Options.CONFIG.genRepr

+          Logger.Info (idt + "    ")

+          if verified then

+            Logger.InfoLine "~~~ VERIFIED ~~~"

+            sol

+          else 

+            Logger.InfoLine "!!! NOT VERIFIED !!!"

+            if Options.CONFIG.inferConditionals then

+              Logger.InfoLine (idt + "    Strengthening the pre-condition")

+              TryInferConditionals (indent + 4) prog comp m unifs heapInst callGraph

+            else

+              sol      

         else

-          sol      

-    else

-      sol

-and TryInferConditionals indent prog comp m unifs heapInst = 

-  // use the orginal method, not the one with an extra precondition

-  let __FixSolution sol =

-    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

+          sol

+and TryInferConditionals indent prog comp m unifs heapInst callGraph = 

   let idt = Indent indent

   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

@@ -388,7 +371,7 @@ and TryInferConditionals indent prog comp m unifs heapInst =
         newCond

     Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

     let _,_,m2 = AddPrecondition prog comp m candCond

-    let sol = MakeModular indent prog comp m2 candCond heapInst2

+    let sol = MakeModular indent prog comp m2 candCond heapInst2 callGraph

     Logger.Info (idt + "    - verifying partial solution ... ")

     let verified = 

       if Options.CONFIG.verifyPartialSolutions then

@@ -397,14 +380,16 @@ and TryInferConditionals indent prog comp m unifs heapInst =
         true

     if verified then

       if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

-      let solThis = match FindExisting indent comp m2 candCond with

+      let solThis = match TryFindExistingAndConvertToSolution indent comp m2 candCond callGraph with

                     | Some(sol2) -> sol2

                     | None -> sol   

       let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

-      let solRest = match FindExisting indent comp m3 (UnaryNot(candCond)) with

-                    | Some(sol3) -> sol3

-                    | None -> AnalyzeConstructor (indent + 2) prog comp m3

-      MergeSolutions (__FixSolution solThis) (__FixSolution solRest)

+      let solRest = AnalyzeConstructor (indent + 2) prog comp m3 callGraph

+//      let solRest = match FindExisting indent comp m3 (UnaryNot(candCond)) with

+//                    | Some(sol3) -> sol3

+//                    | None -> AnalyzeConstructor (indent + 2) prog comp m3

+ 

+      MergeSolutions solThis solRest |> FixSolution m

     else 

       Logger.InfoLine "NOT VERIFIED"

       wrongSol  

@@ -454,11 +439,12 @@ let rec AnalyzeMethods prog members solutionsSoFar =
       | Some(_) -> true

       | None -> false

 

-  let rec __AnalyzeConstructorDeep prog mList solutionsSoFar = 

+  let rec __AnalyzeConstructorDeep prog mList solutionsSoFar =

+    let callGraph = GetCallGraph (solutionsSoFar |> Map.toList) Map.empty

     match mList with

     | (comp,mthd) :: rest -> 

         if not (__IsAlreadySolved comp mthd solutionsSoFar) then

-          let sol = AnalyzeConstructor 2 prog comp mthd

+          let sol = AnalyzeConstructor 2 prog comp mthd callGraph

           let unsolved = sol |> Map.filter (fun (c,m) lst -> lst = [] && not(__IsAlreadySolved c m solutionsSoFar)) |> Utils.MapKeys

           let newSols = solutionsSoFar |> MergeSolutions sol

           __AnalyzeConstructorDeep prog (rest@unsolved) newSols

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index a8a4cda6..85e1fd01 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -251,8 +251,8 @@ let GenConstructorCode mthd body genRepr =
   let validExpr = IdLiteral("Valid()");

   match mthd with

   | Method(methodName, sign, pre, post, _) -> 

-      let preExpr = pre 

-      let postExpr = GetPostconditionForMethod mthd genRepr

+      let preExpr = pre |> Desugar

+      let postExpr = GetPostconditionForMethod mthd genRepr |> Desugar

       "  method " + methodName + (PrintSig sign) + newline +

       "    modifies this;" + 

       (PrintPrePost (newline + "    requires ") preExpr) + 

@@ -273,7 +273,7 @@ let PrintImplCode prog solutions genRepr =
                                                               match sol with

                                                               | [] -> 

                                                                   "    //unable to synthesize" +

-                                                                  PrintPrePost (newline + "    assume ") (GetPostconditionForMethod m genRepr) + newline

+                                                                  PrintPrePost (newline + "    assume ") (GetPostconditionForMethod m genRepr |> Desugar) + newline

                                                               | _ -> 

                                                                   PrintHeapCreationCode prog sol 4 genRepr

                                                             acc + newline + (GenConstructorCode m mthdBody genRepr) + newline

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 668263b9..37b943c6 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/Set.jen /method:SetNode.Triple /genRepr  /genMod</StartArguments>

+    <StartArguments>examples/Number.jen /method:Number.Abs /genRepr  /genMod</StartArguments>

     <StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs
index 54a76139..0f675e4d 100644
--- a/Jennisys/Jennisys/MethodUnifier.fs
+++ b/Jennisys/Jennisys/MethodUnifier.fs
@@ -122,7 +122,10 @@ let rec TryFindAMatch targetMthd candidateMethods =
         | Some(unifs) -> Some(candMthd,unifs)

         | None -> TryFindAMatch targetMthd rest

   | [] -> None

-  

+

+let TryFindExistingOpt comp targetMthd = 

+  TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers)

+

 let TryFindExisting comp targetMthd = 

   match TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with

   | Some(m,unifs) -> m,unifs

@@ -132,4 +135,35 @@ let ApplyMethodUnifs m unifs =
   GetMethodArgs m |> List.map (fun (Var(name,_)) -> 

                                  match Map.tryFind name unifs with

                                  | Some(e) -> e

-                                 | None -> VarLiteral(name))
\ No newline at end of file
+                                 | None -> VarLiteral(name))

+

+let TryFindExistingAndConvertToSolution indent comp m cond callGraph =

+  let __Calls caller callee =

+    let keyOpt = callGraph |> Map.tryFindKey (fun (cc,mm) mset -> CheckSameMethods (comp,caller) (cc,mm))

+    match keyOpt with

+    | Some(k) -> callGraph |> Map.find k |> Set.contains ((GetComponentName comp),(GetMethodName callee))

+    | None -> false

+  (* --- function body starts here --- *)      

+  if not Options.CONFIG.genMod then

+    None

+  else 

+    let idt = Indent indent

+    let candidateMethods = GetMembers comp |> List.filter (fun cm ->

+                                                             match cm with

+                                                             | Method(mname,_,_,_,_) when not (__Calls cm m) -> true

+                                                             | _ -> false)

+    match TryFindAMatch m candidateMethods with

+    | Some(m',unifs) -> 

+        Logger.InfoLine (idt + "    - substitution method found:")

+        Logger.InfoLine (PrintMethodSignFull (indent+6) comp m')

+        let args = ApplyMethodUnifs m' unifs

+        let delegateCall = MethodCall(ThisLiteral, GetMethodName m', args)

+        let obj = { name = "this"; objType = GetClassType comp }

+        let var = Var("", None)

+        let body = [(obj,var), delegateCall]

+        let hInst = { assignments = body; 

+                      methodArgs  = Map.empty; 

+                      globals     = Map.empty }

+        Some(Map.empty |> Map.add (comp,m) [cond, hInst]

+                       |> Map.add (comp,m') [])

+    | None -> None
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs
index 72181c2f..9bb3da72 100644
--- a/Jennisys/Jennisys/Modularizer.fs
+++ b/Jennisys/Jennisys/Modularizer.fs
@@ -28,12 +28,7 @@ let MergeSolutions sol1 sol2 =
   (* --- function body starts here --- *)

   __Merge sol1 (sol2 |> Map.toList) sol1 

                    

-//  =======================================================================

-/// Tries to make a given solution for a given method into more modular, 

-/// by delegating some statements (initialization of inner objects) to 

-/// method calls. 

-//  =======================================================================

-let GetModularBranch prog comp meth hInst = 

+let rec MakeModular indent prog comp meth cond hInst callGraph = 

   let rec __AddDirectChildren e acc = 

     match e with

     | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e

@@ -66,15 +61,33 @@ let GetModularBranch prog comp meth hInst =
   let __GetObjLitType objLitName = 

     (__FindObj objLitName).objType

 

+  //  ===============================================================================

+  /// Goes through the assignments of the heapInstance and returns only those 

+  /// assignments that correspond to abstract fields of the given "objLitName" object

+  //  ===============================================================================

   let __GetAbsFldAssignments objLitName = 

     hInst.assignments |> List.choose (fun ((obj,var),e) ->

                                         if obj.name = objLitName && __IsAbstractField obj.objType var then

                                           Some(var,e)

                                         else

                                           None)

+

+  //  ===============================================================================

+  /// The given assignment is: 

+  ///   x := e

+  ///

+  /// If e is an object (e.g. gensym32) with e.g. two abstract fields "a" and "b", 

+  /// with values 3 and 8 respectively, then the "x := e" spec is fixed as following: 

+  ///   x.a := 3 && x.b := 8

+  /// 

+  /// List values are handled similarly, e.g.:

+  ///   x := [gensym32]

+  /// is translated into

+  ///   |x| = 1 && x[0].a = 3 && x[0].b = 8

+  //  ===============================================================================

   let rec __ExamineAndFix x e = 

     match e with

-    | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> 

+    | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> //TODO: is it really only non-direct children?

         let absFlds = __GetAbsFldAssignments id

         absFlds |> List.fold (fun acc (Var(vname,_),vval) -> BinaryAnd acc (BinaryEq (Dot(x, vname)) vval)) TrueLiteral

     | SequenceExpr(elist) ->

@@ -89,10 +102,19 @@ let GetModularBranch prog comp meth hInst =
         __fff elist TrueLiteral 0

     | _ -> BinaryEq x e

 

+  //  ================================================================================

+  /// The spec for an object consists of assignments to its abstract fields with one 

+  /// caveat: if some assignments include non-direct children objects of "this", then 

+  /// those objects cannot be used directly in the spec; instead, their properties must 

+  /// be expanded and embeded (that's what the "ExamineAndFix" function does)

+  //  ================================================================================

   let __GetSpecFor objLitName =

     let absFieldAssignments = __GetAbsFldAssignments objLitName

     absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

   

+  //  ================================================================================================

+  /// Simply traverses a given expression and returns all arguments of the "meth" method that are used

+  //  ================================================================================================

   let __GetArgsUsed expr = 

     let args = GetMethodArgs meth

     let argSet = DescendExpr2 (fun e acc ->

@@ -121,37 +143,51 @@ let GetModularBranch prog comp meth hInst =
     | _ :: rest -> failwith "internal error: expected to see only ObjLiterals"

     | [] -> acc

 

-  (* --- function body starts here --- *)

-  let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty

-  let initChildrenExprList = delegateMethods |> Map.toList

-                                             |> List.map (fun (receiver, (cmp,mthd,args)) -> 

-                                                            let key = __FindObj (PrintExpr 0 receiver), Var("", None)

-                                                            let e = MethodCall(receiver, GetMethodName mthd, args)

-                                                            (key, e))

-  let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)

-  let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->

-                                                                       let obj = __FindObj (PrintExpr 0 receiver)

-                                                                       match acc with

-                                                                       | accProg, accComp, accmList ->

-                                                                           let oldComp = FindComponent accProg (GetTypeShortName obj.objType) |> Utils.ExtractOption

-                                                                           let prog', mcomp' = AddReplaceMethod accProg oldComp newMthd None

-                                                                           let mList' = (mcomp', newMthd) :: accmList

-                                                                           let comp' = if accComp = oldComp then mcomp' else accComp

-                                                                           prog', comp', mList'

-                                                                    ) (prog, comp, [])

-  newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

+  //  =======================================================================

+  /// Tries to make a given solution for a given method into more modular, 

+  /// by delegating some statements (initialization of inner objects) to 

+  /// method calls. 

+  //  =======================================================================

+  let __GetModularBranch = 

+    let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty

+    let initChildrenExprList = delegateMethods |> Map.toList

+                                                |> List.map (fun (receiver, (cmp,mthd,args)) -> 

+                                                              let key = __FindObj (PrintExpr 0 receiver), Var("", None)

+                                                              let e = MethodCall(receiver, GetMethodName mthd, args)

+                                                              (key, e))

+    let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)

+    let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->

+                                                                          let obj = __FindObj (PrintExpr 0 receiver)

+                                                                          match acc with

+                                                                          | accProg, accComp, accmList ->

+                                                                              let oldComp = FindComponent accProg (GetTypeShortName obj.objType) |> Utils.ExtractOption

+                                                                              let prog', mcomp' = AddReplaceMethod accProg oldComp newMthd None

+                                                                              let mList' = (mcomp', newMthd) :: accmList

+                                                                              let comp' = if accComp = oldComp then mcomp' else accComp

+                                                                              prog', comp', mList'

+                                                                      ) (prog, comp, [])

+    newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

 

-let rec MakeModular indent prog comp m cond heapInst = 

+  (* --- function body starts here --- *)

   let idt = Indent indent

   if Options.CONFIG.genMod then   

     Logger.InfoLine (idt + "    - delegating to method calls     ...")

-    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     

+    // first try to find a match for the entire method (based on the given solution)

+    let postSpec = __GetSpecFor "this"

+    let meth' = match meth with

+                | Method (mname, msig, mpre, _, isConstr) -> Method(mname, msig, mpre, postSpec, isConstr)

+                | _ -> failwithf "internal error: expected a Method but got %O" meth

+    match TryFindExistingAndConvertToSolution indent comp meth' cond callGraph with

+    | Some(sol) -> sol

+    | None -> 

+        // if not found, try to split into parts

+        let _, _, newMthdLst, newHeapInst = __GetModularBranch

+        let msol = Utils.MapSingleton (comp,meth) [cond, newHeapInst]

+        newMthdLst |> List.fold (fun acc (c,m) -> 

+                                   acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 

+                                 ) msol     

   else 

-    Utils.MapSingleton (comp,m) [cond, heapInst]

+    Utils.MapSingleton (comp,meth) [cond, hInst]

 

 //let GetModularSol prog sol = 

 //  let comp = fst (fst sol)

diff --git a/Jennisys/Jennisys/Resolver.fs b/Jennisys/Jennisys/Resolver.fs
index f4d31ccd..46d14746 100644
--- a/Jennisys/Jennisys/Resolver.fs
+++ b/Jennisys/Jennisys/Resolver.fs
@@ -137,4 +137,20 @@ let ResolveModel hModel =
                                       ) Map.empty 

   { assignments = hmap; 

     methodArgs  = argmap; 

-    globals     = Map.empty }
\ No newline at end of file
+    globals     = Map.empty }

+

+let rec GetCallGraph solutions graph = 

+  match solutions with

+  | ((comp,m), sol) :: rest -> 

+        let callees = sol |> List.fold (fun acc (cond, hInst) ->

+                                          let mcalls = hInst.assignments |> List.choose (fun ((obj,_),e) ->

+                                                                                          match e with 

+                                                                                          | MethodCall(_,mname,_) -> 

+                                                                                              let targetCompName = GetTypeShortName obj.objType

+                                                                                              Some(targetCompName, mname)

+                                                                                          | _ -> None)

+                                          acc |> Set.union (mcalls |> Set.ofList)

+                                      ) Set.empty

+        let graph' = graph |> Map.add (comp,m) callees

+        GetCallGraph rest graph'

+  | [] -> graph
\ No newline at end of file
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
index 3f1e6b4b..454a8548 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Number.dfy
@@ -25,116 +25,84 @@ class Number {
   }

 

 

-  method Double(p: int)

+  method Abs(a: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num == 2 * p;

+    ensures num in {a, -a};

+    ensures num >= 0;

   {

-    this.num := 2 * p;

-    // repr stuff

-    this.Repr := {this};

+    if (a >= 0) {

+      this.Init(a);

+    } else {

+      this.Init(-a);

+    }

   }

 

 

-  method Init(p: int)

+  method Double(p: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num == p;

+    ensures num == 2 * p;

   {

-    this.num := p;

-    // repr stuff

-    this.Repr := {this};

+    this.Init(2 * p);

   }

 

 

-  method Sum(a: int, b: int)

+  method Init(p: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num == a + b;

+    ensures num == p;

   {

-    this.num := a + b;

+    this.num := p;

     // repr stuff

     this.Repr := {this};

   }

 

 

-  method Abs(a: int)

+  method Min2(a: int, b: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num in {a, -a};

-    ensures num >= 0;

+    ensures a < b ==> num == a;

+    ensures a >= b ==> num == b;

   {

-    if (a >= 0) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

+    if (a >= b ==> a == b) {

+      this.Init(a);

     } else {

-      this.num := -a;

-      // repr stuff

-      this.Repr := {this};

+      this.Init(b);

     }

   }

 

 

-  method Min4(a: int, b: int, c: int, d: int)

+  method Min22(a: int, b: 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);

+    ensures num in {a, b};

+    ensures num <= a;

+    ensures num <= b;

   {

-    if (a <= b && (a <= c && a <= d)) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

+    if (a <= b) {

+      this.Init(a);

     } 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};

-        }

-      }

+      this.Init(b);

     }

   }

 

 

-  method MinSum(a: int, b: int, c: int)

+  method Min3(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;

+    ensures num in {a, b, c};

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= 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};

-      }

-    }

+    this.Min32(a, b, c);

   }

 

 

@@ -143,89 +111,68 @@ class Number {
     ensures fresh(Repr - {this});

     ensures Valid();

     ensures num in {a, b, c};

-    ensures (forall x :: x in {a, b, c} ==> num <= x);

+    ensures num <= a;

+    ensures num <= b;

+    ensures num <= c;

   {

     if (a <= b && a <= c) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

+      this.Init(a);

     } else {

       if (c <= a && c <= b) {

-        this.num := c;

-        // repr stuff

-        this.Repr := {this};

+        this.Init(c);

       } else {

-        this.num := b;

-        // repr stuff

-        this.Repr := {this};

+        this.Init(b);

       }

     }

   }

 

 

-  method Min3(a: int, b: int, c: int)

+  method Min4(a: int, b: int, c: int, d: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num in {a, b, c};

+    ensures num in {a, b, c, d};

     ensures num <= a;

     ensures num <= b;

     ensures num <= c;

+    ensures num <= d;

   {

-    if (a <= b && a <= c) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

+    if (a <= b && (a <= c && a <= d)) {

+      this.Init(a);

     } else {

-      if (c <= a && c <= b) {

-        this.num := c;

-        // repr stuff

-        this.Repr := {this};

+      if (d <= a && (d <= b && d <= c)) {

+        this.Init(d);

       } else {

-        this.num := b;

-        // repr stuff

-        this.Repr := {this};

+        if (c <= a && (c <= b && c <= d)) {

+          this.Init(c);

+        } else {

+          this.Init(b);

+        }

       }

     }

   }

 

 

-  method Min22(a: int, b: int)

+  method MinSum(a: int, b: int, c: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures num in {a, b};

-    ensures num <= a;

-    ensures num <= b;

+    ensures num in {a + b, a + c, b + c};

+    ensures num <= a + b;

+    ensures num <= b + c;

+    ensures num <= a + c;

   {

-    if (a <= b) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

-    } else {

-      this.num := b;

-      // repr stuff

-      this.Repr := {this};

-    }

+    this.Min3(a + b, a + c, b + c);

   }

 

 

-  method Min2(a: int, b: int)

+  method Sum(a: int, b: int)

     modifies this;

     ensures fresh(Repr - {this});

     ensures Valid();

-    ensures a < b ==> num == a;

-    ensures a >= b ==> num == b;

+    ensures num == a + b;

   {

-    if (a >= b ==> a == b) {

-      this.num := a;

-      // repr stuff

-      this.Repr := {this};

-    } else {

-      this.num := b;

-      // repr stuff

-      this.Repr := {this};

-    }

+    this.Init(a + b);

   }

 

 }

diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
index c9584a5f..8449b03c 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -78,12 +78,7 @@ class Set {
     ensures Valid();

     ensures elems == {p + q};

   {

-    var gensym69 := new SetNode;

-    gensym69.Init(p + q);

-    this.elems := {p + q};

-    this.root := gensym69;

-    // repr stuff

-    this.Repr := {this} + this.root.Repr;

+    this.Singleton(p + q);

   }

 

 }

@@ -169,6 +164,27 @@ class SetNode {
   }

 

 

+  method TripleBase(x: int, y: int, z: int)

+    modifies this;

+    requires x < y;

+    requires y < z;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y, z};

+  {

+    var gensym80 := new SetNode;

+    var gensym81 := new SetNode;

+    gensym80.Init(z);

+    gensym81.Init(x);

+    this.data := y;

+    this.elems := {x, y, z};

+    this.left := gensym81;

+    this.right := gensym80;

+    // repr stuff

+    this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+  }

+

+

   method Double(x: int, y: int)

     modifies this;

     requires x != y;

@@ -216,27 +232,6 @@ class SetNode {
     this.Repr := {this};

   }

 

-

-  method TripleBase(x: int, y: int, z: int)

-    modifies this;

-    requires x < y;

-    requires y < z;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x, y, z};

-  {

-    var gensym80 := new SetNode;

-    var gensym81 := new SetNode;

-    gensym80.Init(z);

-    gensym81.Init(x);

-    this.data := y;

-    this.elems := {x, y, z};

-    this.left := gensym81;

-    this.right := gensym80;

-    // repr stuff

-    this.Repr := ({this} + this.left.Repr) + this.right.Repr;

-  }

-

 }