- added synthesis of Repr stuff (it generates Repr invariants,

   and updates the Repr fields at the end of every constructor)

 - refactoring:
    - removed ExprConst
    - change the implementation to use HeapModel and HeapInstance
      (as opposed to propagating heap/env/ctx)

15 files changed, 565 insertions, 403 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 9603dd6e..2bbd43cf 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -13,13 +13,7 @@ open Utils
 

 open Microsoft.Boogie

 

-type MethodSolution = {

-   pathCond: Expr; 

-   heap : Map<Const * VarDecl, Const>; 

-   env  : Map<Const, Const>; 

-   ctx  : Set<Set<Const>>;

-}

-                    

+                  

 let Rename suffix vars =

   vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))

 

@@ -92,7 +86,7 @@ let rec IsArgsOnly args expr =
   | ForallExpr(vars,e)                   -> IsArgsOnly (List.concat [args; vars]) e

 

 //TODO: unifications should probably by "Expr <--> Expr" instead of "Expr <--> Const"

-let GetUnifications indent expr args (heap,env,ctx) =

+let GetUnifications indent expr args heapInst =

   let idt = Indent indent

   // - first looks if the give expression talks only about method arguments (args)

   // - then checks if it doesn't already exist in the unification map

@@ -103,8 +97,8 @@ let GetUnifications indent expr args (heap,env,ctx) =
     builder {

       let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption

       let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption

-      let! v = try Some(Eval (heap,env,ctx) true e |> Expr2Const) with ex -> None

-      Logger.DebugLine (idt + "    - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));

+      let! v = try Some(Eval heapInst true e |> Expr2Const) with ex -> None

+      Logger.DebugLine (idt + "    - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v))

       return Map.add e v unifMap

     }

   // just recurses on all expressions

@@ -134,15 +128,15 @@ let GetUnifications indent expr args (heap,env,ctx) =
 /// Returns a map (Expr |--> Const) containing unifications

 /// found for the given method and heap/env/ctx

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

-let GetUnificationsForMethod indent comp m (heap,env,ctx) =

+let GetUnificationsForMethod indent comp m heapInst =

   let idt = Indent indent

-  let rec GetArgValueUnifications args env = 

+  let rec GetArgValueUnifications args = 

     match args with

     | Var(name,_) :: rest -> 

-        match Map.tryFind (Unresolved(name)) env with

+        match Map.tryFind name heapInst.methodArgs with

         | Some(c) ->

-            Logger.DebugLine (idt + "    - adding unification " + (PrintConst c) + " <--> " + name);

-            Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)

+            Logger.DebugLine (idt + "    - adding unification " + name + " <--> " + (PrintConst c));

+            Map.ofList [VarLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest)

         | None -> failwith ("couldn't find value for argument " + name)

     | [] -> Map.empty

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

@@ -151,8 +145,8 @@ let GetUnificationsForMethod indent comp m (heap,env,ctx) =
       let args = List.concat [ins; outs]

       match args with 

       | [] -> Map.empty

-      | _  -> GetUnifications indent (BinaryAnd pre post) args (heap,env,ctx)

-              |> Utils.MapAddAll (GetArgValueUnifications args env)

+      | _  -> GetUnifications indent (BinaryAnd pre post) args heapInst

+              |> Utils.MapAddAll (GetArgValueUnifications args)

   | _ -> failwith ("not a method: " + m.ToString())

 

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

@@ -163,33 +157,32 @@ let GetUnificationsForMethod indent comp m (heap,env,ctx) =
 /// path.  It starts from the given object, and follows the backpointers

 /// until it reaches the root ("this")

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

-let objRef2ExprCache = new System.Collections.Generic.Dictionary<Const, Expr>()

-let GetObjRefExpr o (heap,env,ctx) = 

-  let rec __GetObjRefExpr o (heap,env,ctx) visited = 

-    if Set.contains o visited then 

+let objRef2ExprCache = new System.Collections.Generic.Dictionary<string, Expr>()

+let GetObjRefExpr objRefName (heapInst: HeapInstance) = 

+  let rec __GetObjRefExpr objRefName visited = 

+    if Set.contains objRefName visited then 

       None

     else 

-      let newVisited = Set.add o visited

-      let refName = PrintObjRefName o (env,ctx)

-      match refName with

+      let newVisited = Set.add objRefName visited

+      match objRefName with

       | "this" -> Some(ObjLiteral("this"))

       | _ -> 

           let rec __fff lst = 

             match lst with

-            | ((o,Var(fldName,_)),l) :: rest -> 

-                match __GetObjRefExpr o (heap,env,ctx) newVisited with

+            | ((o,Var(fldName,_)),_) :: rest -> 

+                match __GetObjRefExpr o.name newVisited with

                 | Some(expr) -> Some(Dot(expr, fldName))

                 | None -> __fff rest

             | [] -> None

-          let backPointers = heap |> Map.filter (fun (_,_) l -> l = o) |> Map.toList

+          let backPointers = heapInst.assignments |> Map.filter (fun (_,_) l -> l = ObjLiteral(objRefName)) |> Map.toList

           __fff backPointers 

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

-  if objRef2ExprCache.ContainsKey(o) then

-    Some(objRef2ExprCache.[o])

+  if objRef2ExprCache.ContainsKey(objRefName) then

+    Some(objRef2ExprCache.[objRefName])

   else

-    let res = __GetObjRefExpr o (heap,env,ctx) (Set.empty)

+    let res = __GetObjRefExpr objRefName (Set.empty)

     match res with 

-    | Some(e) -> objRef2ExprCache.Add(o, e)

+    | Some(e) -> objRef2ExprCache.Add(objRefName, e)

     | None -> ()

     res

 

@@ -199,13 +192,13 @@ let GetObjRefExpr o (heap,env,ctx) =
 /// If "conservative" is true, applies only those that 

 /// can be verified to hold, otherwise applies all of them

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

-let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservative = 

+let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative = 

   let idt = Indent indent

   let __CheckUnif o f e idx =

     if not conservative || not Options.CONFIG.checkUnifications then 

       true 

     else

-      let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + (PrintObjRefName o (env,ctx)))

+      let objRefExpr = GetObjRefExpr o heapInst |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + o)

       let fldName = PrintVarName f                             

       let lhs = Dot(objRefExpr, fldName)

       let assertionExpr = match f with

@@ -213,7 +206,7 @@ let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservativ
                           | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs

                           | _                                            -> BinaryEq lhs e 

       // check if the assertion follows and if so update the env

-      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)

+      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr) false

       Logger.Debug (idt + "    - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")

       let ok = CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))

       if ok then

@@ -224,50 +217,49 @@ let rec ApplyUnifications indent prog comp mthd unifs (heap,env,ctx) conservativ
   (* --- function body starts here --- *)

   match unifs with

   | (e,c) :: rest -> 

-      let restHeap,env,ctx = ApplyUnifications indent prog comp mthd rest (heap,env,ctx) conservative

-      let newHeap = restHeap |> Map.fold (fun acc (o,f) l ->

-                                            let value = TryResolve (env,ctx) l

-                                            if value = c then

-                                              if __CheckUnif o f e -1 then                                                

-                                                // change the value to expression

-                                                //Logger.TraceLine (sprintf "%s    - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

-                                                acc |> Map.add (o,f) (ExprConst(e))

-                                              else

-                                                // don't change the value unless "conservative = false"

-                                                acc |> Map.add (o,f) l

-                                            else 

-                                              let rec __UnifyOverLst lst cnt =

-                                                    match lst with

-                                                    | lstElem :: rest when lstElem = c ->

-                                                        if __CheckUnif o f e cnt then

-                                                          //Logger.TraceLine (sprintf "%s    - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )

-                                                          ExprConst(e) :: __UnifyOverLst rest (cnt+1)

-                                                        else  

-                                                          lstElem :: __UnifyOverLst rest (cnt+1)

-                                                    | lstElem :: rest ->

-                                                        lstElem :: __UnifyOverLst rest (cnt+1)

-                                                    | [] -> []

-                                              // see if it's a list, then try to match its elements, otherwise leave it as is

-                                              match value with

-                                              | SeqConst(clist) -> 

-                                                  let newLstConst = __UnifyOverLst clist 0

-                                                  acc |> Map.add (o,f) (SeqConst(newLstConst))

-                                              | SetConst(cset) ->

-                                                  let newLstConst = __UnifyOverLst (Set.toList cset) 0

-                                                  acc |> Map.add (o,f) (SetConst(newLstConst |> Set.ofList))

-                                              | _ -> 

-                                                  acc |> Map.add (o,f) l

-                                         ) restHeap

-      (newHeap,env,ctx)

-  | [] -> (heap,env,ctx)

+      let heapInst = ApplyUnifications indent prog comp mthd rest heapInst conservative

+      let newHeap = heapInst.assignments|> Map.fold (fun acc (o,f) value ->

+                                                       if value = Const2Expr c then

+                                                         if __CheckUnif o.name f e -1 then                                                

+                                                           // change the value to expression

+                                                           //Logger.TraceLine (sprintf "%s    - applied: %s.%s --> %s" idt (PrintConst o) (GetVarName f) (PrintExpr 0 e) )

+                                                           acc |> Map.add (o,f) e

+                                                         else

+                                                           // don't change the value unless "conservative = false"

+                                                           acc |> Map.add (o,f) value

+                                                       else 

+                                                         let rec __UnifyOverLst lst cnt =

+                                                               match lst with

+                                                               | lstElem :: rest when lstElem = Const2Expr c ->

+                                                                   if __CheckUnif o.name f e cnt then

+                                                                     //Logger.TraceLine (sprintf "%s    - applied: %s.%s[%d] --> %s" idt (PrintConst o) (GetVarName f) cnt (PrintExpr 0 e) )

+                                                                     e :: __UnifyOverLst rest (cnt+1)

+                                                                   else  

+                                                                     lstElem :: __UnifyOverLst rest (cnt+1)

+                                                               | lstElem :: rest ->

+                                                                   lstElem :: __UnifyOverLst rest (cnt+1)

+                                                               | [] -> []

+                                                         // see if it's a list, then try to match its elements, otherwise leave it as is

+                                                         match value with

+                                                         | SequenceExpr(elist) -> 

+                                                             let newExprList = __UnifyOverLst elist 0

+                                                             acc |> Map.add (o,f) (SequenceExpr(newExprList))

+                                                         | SetExpr(elist) ->

+                                                             let newExprList = __UnifyOverLst elist 0

+                                                             acc |> Map.add (o,f) (SetExpr(newExprList))

+                                                         | _ -> 

+                                                             acc |> Map.add (o,f) value

+                                                     ) heapInst.assignments

+      {heapInst with assignments = newHeap }

+  | [] -> heapInst

 

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

 /// Returns whether the code synthesized for the given method can be verified with Dafny

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

-let VerifySolution prog comp mthd sol =

+let VerifySolution prog comp mthd sol genRepr =

   // print the solution to file and try to verify it with Dafny

   let solutions = Map.empty |> Map.add (comp,mthd) sol

-  let code = PrintImplCode prog solutions (fun p -> [comp,mthd])

+  let code = PrintImplCode prog solutions (fun p -> [comp,mthd]) genRepr

   CheckDafnyProgram code dafnyVerifySuffix

 

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

@@ -280,7 +272,7 @@ let rec AnalyzeConstructor indent prog comp m =
   let methodName = GetMethodName m

   let pre,post = GetMethodPrePost m

   // generate Dafny code for analysis first

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

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

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

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

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

@@ -297,13 +289,14 @@ let rec AnalyzeConstructor indent prog comp m =
       failwith "internal error (more than one model for a single constructor analysis)"

     Logger.InfoLine " OK "

     let model = models.[0]

-    let heap,env,ctx = ReadFieldValuesFromModel model prog comp m

-    let unifs = GetUnificationsForMethod indent comp m (heap,env,ctx) |> Map.toList

-    let heap,env,ctx = ApplyUnifications indent prog comp m unifs (heap,env,ctx) true

+    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

     if Options.CONFIG.verifySolutions then

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

-      let sol = [TrueLiteral, (heap,env,ctx)]

-      let verified = VerifySolution prog comp m sol

+      let sol = [TrueLiteral, heapInst]

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

       Logger.Info (idt + "    ")

       if verified then

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

@@ -311,50 +304,53 @@ let rec AnalyzeConstructor indent prog comp m =
       else 

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

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

-        TryInferConditionals (indent + 4) prog comp m unifs (heap,env,ctx)

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

     else

-      [TrueLiteral, (heap,env,ctx)]

-and TryInferConditionals indent prog comp m unifs (heap,env,ctx) = 

+      [TrueLiteral, heapInst]

+and TryInferConditionals indent prog comp m unifs heapInst = 

   let idt = Indent indent

-  let heap2,env2,ctx2 = ApplyUnifications indent prog comp m unifs (heap,env,ctx) false

+  let wrongSol = [TrueLiteral, heapInst]

+  let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

   // get expressions to evaluate:

-  //   - add pre and post conditions                                     

-  //   - go through all objects on the heap and assert its invariant  

+  //   - add post (and pre?) conditions                                     

+  //   - go through all objects on the heap and assert their invariants  

   let pre,post = GetMethodPrePost m

   let prepostExpr = post //TODO: do we need the "pre" here as well?

-  let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty

+  let heapObjs = heapInst2.assignments |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty

   let expr = heapObjs |> Set.fold (fun acc o -> 

-                                     let receiverOpt = GetObjRefExpr o (heap,env,ctx) 

+                                     let receiverOpt = GetObjRefExpr o.name heapInst2

                                      let receiver = Utils.ExtractOption receiverOpt

-                                     match Resolve (env,ctx) o with

-                                     | NewObj(_,tOpt) | ThisConst(_,tOpt) ->

-                                         let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt

-                                         let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption

-                                         let objInvs = GetInvariantsAsList objComp

-                                         let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

-                                         objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

-                                     | _ -> failwith "not supposed to happen"

+                                     let objComp = FindComponent prog (GetTypeShortName o.objType) |> Utils.ExtractOption

+                                     let objInvs = GetInvariantsAsList objComp

+                                     let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

+                                     objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

                                   ) prepostExpr

-  //expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")

   // now evaluate and see what's left

-  let newCond = Eval (heap2,env2,ctx2) false expr

+  let newCond = Eval heapInst2 false expr

   try

     if newCond = TrueLiteral then

       Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

-      []

+      wrongSol

     else

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

       let p2,c2,m2 = AddPrecondition prog comp m newCond

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

-      let sol = [newCond, (heap2,env2,ctx2)]

-      let verified = VerifySolution p2 c2 m2 sol

+      let sol = [newCond, heapInst2]

+      let verified = 

+        if Options.CONFIG.verifyPartialSolutions then

+          VerifySolution p2 c2 m2 sol Options.CONFIG.genRepr

+        else 

+          true

       if verified then

-        Logger.InfoLine "VERIFIED"

+        if Options.CONFIG.verifyPartialSolutions then

+          Logger.InfoLine "VERIFIED"

+        else 

+          Logger.InfoLine "SKIPPED"

         let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(newCond))

         sol.[0] :: AnalyzeConstructor (indent + 2) p3 c3 m3

       else 

         Logger.InfoLine "NOT VERIFIED"

-        []                     

+        wrongSol                     

   with

     ex -> raise ex

 

@@ -410,7 +406,7 @@ let Analyze prog filename =
   use file = System.IO.File.CreateText(dafnySynthFileNameTemplate.Replace("###", progName))

   file.AutoFlush <- true

   Logger.InfoLine "Printing synthesized code"

-  let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze

+  let synthCode = PrintImplCode prog solutions GetMethodsToAnalyze Options.CONFIG.genRepr

   fprintfn file "%s" synthCode

   ()

 

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index 1ddf1f31..b9105254 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -56,7 +56,6 @@ type Const =
   | ThisConst  of (* loc id *) string * Type option

   | VarConst   of string

   | NewObj     of (* loc id *) string * Type option

-  | ExprConst  of Expr

   | Unresolved of (* loc id *) string 

 

 type Stmt =

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 25d2a129..ab86324b 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -9,6 +9,9 @@ module AstUtils
 open Ast

 open Utils

 

+let PrintGenSym name =

+  sprintf "gensym%s" name

+

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

 /// Returns TRUE literal

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

@@ -30,6 +33,12 @@ let UnaryNot sub =
   | _ -> UnaryExpr("!", sub)

 

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

+/// Returns a binary PLUS of the two given expressions

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

+let BinaryPlus (lhs: Expr) (rhs: Expr) = 

+  BinaryExpr(50, "+", lhs, rhs)

+

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

 /// Returns a binary AND of the two given expressions with short-circuiting

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

 let BinaryAnd (lhs: Expr) (rhs: Expr) = 

@@ -62,37 +71,6 @@ let BinaryImplies lhs rhs =
   | _, BoolLiteral(false) -> UnaryNot(lhs)

   | _ -> BinaryExpr(20, "==>", lhs, rhs)

 

-

-//let TrueLiteral = IdLiteral("true")

-//let FalseLiteral = IdLiteral("false")

-//

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

-///// Returns a binary AND of the two given expressions with short-circuiting

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

-//let BinaryAnd (lhs: Expr) (rhs: Expr) = 

-//    match lhs, rhs with

-//    | IdLiteral("true"), _  -> rhs

-//    | IdLiteral("false"), _ -> IdLiteral("false")

-//    | _, IdLiteral("true")  -> lhs

-//    | _, IdLiteral("false") -> IdLiteral("false")

-//    | _, _                  -> BinaryExpr(30, "&&", lhs, rhs)

-//

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

-///// Returns a binary OR of the two given expressions with short-circuiting

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

-//let BinaryOr (lhs: Expr) (rhs: Expr) = 

-//    match lhs, rhs with

-//    | IdLiteral("true"), _  -> IdLiteral("true")

-//    | IdLiteral("false"), _ -> rhs

-//    | _, IdLiteral("true")  -> IdLiteral("true")

-//    | _, IdLiteral("false") -> lhs

-//    | _, _                  -> BinaryExpr(30, "||", lhs, rhs)

-//

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

-///// Returns a binary IMPLIES of the two given expressions (TODO: with short-circuiting)

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

-//let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)

-

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

 /// Constructors for binary EQ/NEQ of two given expressions

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

@@ -100,6 +78,11 @@ let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)
 let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)

 

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

+/// Constructor for binary GETS

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

+let BinaryGets lhs rhs = Assign(lhs, rhs)

+

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

 /// Constructors for binary IN/!IN of two given expressions

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

 let BinaryIn lhs rhs = BinaryExpr(40, "in", lhs, rhs)

@@ -134,11 +117,10 @@ let rec Const2Expr c =
       let expSet = cset |> Set.fold (fun acc c -> Set.add (Const2Expr c) acc) Set.empty

       SetExpr(Set.toList expSet)

   | VarConst(id) -> VarLiteral(id)

-  | ThisConst(name,_) 

-  | NewObj(name,_)   -> ObjLiteral(name)

+  | ThisConst(_,_) -> ObjLiteral("this")

+  | NewObj(name,_) -> ObjLiteral(PrintGenSym name)

   | NullConst -> ObjLiteral("null")

-  | ExprConst(e) -> e

-  | Unresolved(name) -> printf "What about unresolved stuff??"; failwith "don't want to convert unresolved to expr"

+  | Unresolved(name) -> failwithf "don't want to convert unresolved(%s) to expr" name // IdLiteral(name) //

   | _ -> failwithf "not implemented or not supported: %O" c

 

 let rec Expr2Const e =

@@ -147,7 +129,7 @@ let rec Expr2Const e =
   | BoolLiteral(b) -> BoolConst(b)

   | ObjLiteral("this") -> ThisConst("this",None)

   | ObjLiteral("null") -> NullConst

-  | ObjLiteral(name) -> NewObj(name, None) //TODO: or Unresolved?

+  | ObjLiteral(name) -> Unresolved(name)

   | IdLiteral(id) -> Unresolved(id)

   | VarLiteral(id) -> VarConst(id)

   | SequenceExpr(elist) -> SeqConst(elist |> List.map Expr2Const)

@@ -314,13 +296,36 @@ let FindMethod comp methodName =
 //  ==============================================

 /// Finds a field of a class that has a given name

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

-let FindVar (prog: Program) clsName fldName =

-  let copt = FindComponent prog clsName

-  match copt with

-  | Some(comp) -> 

-      GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

-                        |> Utils.ListToOption

-  | None -> None

+//let FindCompVar prog clsName fldName =

+//  let copt = FindComponent prog clsName

+//  match copt with

+//  | Some(comp) -> 

+//      GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

+//                        |> Utils.ListToOption

+//  | None -> None

+

+let FindVar comp fldName =

+  GetAllFields comp |> List.filter (function Var(name,_) when name = fldName -> true | _ -> false)

+                    |> Utils.ListToOption

+

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

+/// Returns the frame of a given component

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

+let GetFrame comp = 

+  match comp with 

+  | Component(_, Model(_,_,_,frame,_), _) -> frame

+  | _ -> failwithf "not a valid component %O" comp

+

+let GetFrameFields comp =

+  let frame = GetFrame comp

+  frame |> List.choose (function IdLiteral(name) -> Some(name) | _ -> None) // TODO: is it really enough to handle only IdLiteral's

+        |> List.choose (fun varName -> 

+                          let v = FindVar comp varName

+                          Utils.ExtractOptionMsg ("field not found: " + varName) v |> ignore

+                          v

+                       )

+

+////////////////////////

 

 let AddPrecondition prog comp m e =

   match prog, comp, m with

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 5d7f8611..f2d5766c 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -7,9 +7,9 @@ open Printer
 open Resolver

 open TypeChecker

 open DafnyPrinter

+open DafnyModelUtils

 

-let numLoopUnrolls = 2

-

+// TODO: this should take a list of fields and unroll all possibilities (instead of unrolling on branch only, following exactly one field)

 let rec GetUnrolledFieldValidExpr fldExpr fldName validFunName numUnrolls : Expr = 

   if numUnrolls = 0 then

     TrueLiteral

@@ -30,12 +30,12 @@ let GetFieldsValidExprList clsName allFields prog : Expr list =
   fields |> List.map (function Var(name, t) -> 

                                  let validFunName, numUnrolls = 

                                    match t with

-                                   | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", numLoopUnrolls

+                                   | Some(ty) when clsName = (GetTypeShortName ty) -> "Valid_self()", Options.CONFIG.numLoopUnrolls

                                    | _ -> "Valid()", 1

                                  GetFieldValidExpr name validFunName numUnrolls

                      )

 

-let PrintValidFunctionCode comp prog : string = 

+let PrintValidFunctionCode comp prog genRepr: string = 

   let idt = "    "

   let __PrintInvs invs = 

     invs |> List.fold (fun acc e -> List.concat [acc ; SplitIntoConjunts e]) []

@@ -45,16 +45,33 @@ let PrintValidFunctionCode comp prog : string =
   let vars = GetAllFields comp

   let allInvs = GetInvariantsAsList comp |> DesugarLst

   let fieldsValid = GetFieldsValidExprList clsName vars prog

-                                                                

+  

+  let frameFldNames = GetFrameFields comp |> List.choose (function Var(name,_) -> Some(name))

+  let validReprBody = 

+    "    this in Repr &&" + newline +

+    "    null !in Repr" + 

+    (PrintSep "" (fun x -> " &&" + newline + "    ($x != null ==> $x in Repr && $x.Repr <= Repr && this !in $x.Repr)".Replace("$x", x)) frameFldNames)

+

+  let vr = 

+    if genRepr then

+      "  function Valid_repr(): bool" + newline +

+      "    reads *;" + newline +

+      "  {" + newline +

+      validReprBody + newline +

+      "  }" + newline + newline

+    else

+      ""                                                        

   // TODO: don't hardcode decr vars!!!

 //  let decrVars = if List.choose (function Var(n,_) -> Some(n)) vars |> List.exists (fun n -> n = "next") then

 //                   ["list"]

 //                 else

 //                   []

 //  (if List.isEmpty decrVars then "" else sprintf "    decreases %s;%s" (PrintSep ", " (fun a -> a) decrVars) newline) +

+  vr + 

   "  function Valid_self(): bool" + newline +

   "    reads *;" + newline +

   "  {" + newline + 

+  (Utils.Ite genRepr ("    Valid_repr() &&" + newline) "") +

   (__PrintInvs allInvs) + newline +

   "  }" + newline +

   newline +

@@ -65,13 +82,12 @@ let PrintValidFunctionCode comp prog : string =
   (__PrintInvs fieldsValid) + newline +

   "  }" + newline

 

-let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =

+let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =

   match prog with

   | Program(components) -> components |> List.fold (fun acc comp -> 

       match comp with  

       | Component(Class(name,typeParams,members), Model(_,_,cVars,frame,inv), code) as comp ->

-        let aVars = FilterFieldMembers members

-        let allVars = List.concat [aVars ; cVars];

+        let aVars = FilterFieldMembers members |> List.append (Utils.Ite genRepr [Var("Repr", Some(SetType(NamedType("object", []))))] [])

         let compMethods = FilterConstructorMembers members

         // Now print it as a Dafny program

         acc + 

@@ -80,92 +96,118 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc: string =
         (sprintf "%s" (PrintFields aVars 2 true)) + newline +     

         (sprintf "%s" (PrintFields cVars 2 false)) + newline +                           

         // generate the Valid function

-        (sprintf "%s" (PrintValidFunctionCode comp prog)) + newline +

+        (sprintf "%s" (PrintValidFunctionCode comp prog genRepr)) + newline +

         // call the method printer function on all methods of this component

         (compMethods |> List.fold (fun acc m -> acc + (methodPrinterFunc comp m)) "") +

         // the end of the class

         "}" + newline + newline

       | _ -> assert false; "") ""

-  

-let PrintAllocNewObjects (heap,env,ctx) indent = 

-  let idt = Indent indent

-  env |> Map.fold (fun acc l v ->

-                     match v with 

-                     | NewObj(_,_) -> acc |> Set.add v

-                     | _ -> acc

-                  ) Set.empty

-      |> Set.fold (fun acc newObjConst ->

-                    match newObjConst with

-                    | NewObj(name, Some(tp)) -> acc + (sprintf "%svar %s := new %s;%s" idt (PrintGenSym name) (PrintType tp) newline)

-                    | _ -> failwithf "NewObj doesn't have a type: %O" newObjConst

-                  ) ""

 

-let PrintObjRefName o (env,ctx) = 

-  match Resolve (env,ctx) o with

-  | ThisConst(_,_) -> "this";

-  | NewObj(name, _) -> PrintGenSym name

-  | _ -> failwith ("unresolved object ref: " + o.ToString())

-

-let CheckUnresolved c =

-  match c with 

-  | Unresolved(_) -> Logger.WarnLine "!!! There are some unresolved constants in the output file !!!"; c 

-  | _ -> c

+let PrintAllocNewObjects heapInst indent = 

+  let idt = Indent indent

+  heapInst.assignments |> Map.fold (fun acc (obj,fld) _ ->

+                                      if not (obj.name = "this") then

+                                        acc |> Set.add obj

+                                      else 

+                                        acc

+                                   ) Set.empty

+                       |> Set.fold (fun acc obj -> acc + (sprintf "%svar %s := new %s;%s" idt obj.name (PrintType obj.objType) newline)) ""

 

-let PrintVarAssignments (heap,env,ctx) indent = 

+let PrintVarAssignments heapInst indent = 

   let idt = Indent indent

-  heap |> Map.fold (fun acc (o,f) l ->

-                      let objRef = PrintObjRefName o (env,ctx)

-                      let fldName = PrintVarName f

-                      let value = TryResolve (env,ctx) l |> CheckUnresolved |> PrintConst

-                      acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline

-                   ) ""

+  heapInst.assignments |> Map.fold (fun acc (o,f) e ->

+                                      let fldName = PrintVarName f

+                                      let value = PrintExpr 0 e

+                                      acc + (sprintf "%s%s.%s := %s;" idt o.name fldName value) + newline

+                                    ) ""

 

-let rec PrintHeapCreationCode sol indent =    

+let PrintReprAssignments prog heapInst indent = 

+  let __FollowsFunc o1 o2 = 

+    heapInst.assignments |> Map.fold (fun acc (srcObj,fld) value -> 

+                                        acc || (srcObj = o1 && value = ObjLiteral(o2.name))

+                                     ) false

+  let idt = Indent indent

+  let objs = heapInst.assignments |> Map.fold (fun acc (obj,fld) _ -> acc |> Set.add obj) Set.empty

+                                  |> Set.toList

+                                  |> Utils.TopSort __FollowsFunc

+                                  |> List.rev

+  let reprGetsList = objs |> List.fold (fun acc obj -> 

+                                          let expr = SetExpr([ObjLiteral(obj.name)])

+                                          let builder = CascadingBuilder<_>(expr)

+                                          let fullRhs = builder {

+                                            let typeName = GetTypeShortName obj.objType

+                                            let! comp = FindComponent prog typeName

+                                            let vars = GetFrameFields comp

+                                            let nonNullVars = vars |> List.filter (fun v -> 

+                                                                                      match Map.tryFind (obj,v) heapInst.assignments with

+                                                                                      | Some(ObjLiteral(n)) when not (n = "null") -> true

+                                                                                      | _ -> false)

+                                            return nonNullVars |> List.fold (fun a v -> 

+                                                                               BinaryPlus a (Dot(Dot(ObjLiteral(obj.name), (PrintVarName v)), "Repr"))

+                                                                            ) expr

+                                          }

+                                          let fullReprExpr = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) fullRhs 

+                                          fullReprExpr :: acc

+                                       ) []

+  

+  idt + "// repr stuff" + newline + 

+  (PrintStmtList reprGetsList indent)

+                                                          

+let rec PrintHeapCreationCode prog sol indent genRepr =    

   let idt = Indent indent

   match sol with

-  | (c, (heap,env,ctx)) :: rest ->

+  | (c, heapInst) :: rest ->

+      let __ReprAssignments ind = 

+        if genRepr then

+          (PrintReprAssignments prog heapInst ind)

+        else 

+          ""

       if c = TrueLiteral then

-        (PrintAllocNewObjects (heap,env,ctx) indent) +

-        (PrintVarAssignments (heap,env,ctx) indent) +

-        newline + 

-        (PrintHeapCreationCode rest indent) 

+        (PrintAllocNewObjects heapInst indent) +

+        (PrintVarAssignments heapInst indent) +

+        (__ReprAssignments indent) +

+        (PrintHeapCreationCode prog rest indent genRepr) 

       else

         if List.length rest > 0 then

           idt + "if (" + (PrintExpr 0 c) + ") {" + newline +

-          (PrintAllocNewObjects (heap,env,ctx) (indent+2)) +

-          (PrintVarAssignments (heap,env,ctx) (indent+2)) +

+          (PrintAllocNewObjects heapInst (indent+2)) +

+          (PrintVarAssignments heapInst (indent+2)) +

+          (__ReprAssignments (indent+2)) +

           idt + "} else {" + newline + 

-          (PrintHeapCreationCode rest (indent+2)) +

+          (PrintHeapCreationCode prog rest (indent+2) genRepr) +

           idt + "}" + newline

         else 

-          (PrintAllocNewObjects (heap,env,ctx) indent) +

-          (PrintVarAssignments (heap,env,ctx) indent)

+          (PrintAllocNewObjects heapInst indent) +

+          (PrintVarAssignments heapInst indent) +

+          (__ReprAssignments indent)

   | [] -> ""

 

-let GenConstructorCode mthd body =

+let GenConstructorCode mthd body genRepr =

   let validExpr = IdLiteral("Valid()");

   match mthd with

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

-      let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")

+      let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep "" (fun e -> pfix + (PrintExpr 0 e) + ";")

       let preExpr = pre 

       let postExpr = BinaryAnd validExpr post

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

-      "    modifies this;" + newline +

-      (__PrintPrePost "    requires " preExpr) + newline +

-      (__PrintPrePost "    ensures " postExpr) + newline +

+      "    modifies this;" + 

+      (__PrintPrePost (newline + "    requires ") preExpr) + 

+      Utils.Ite genRepr (newline + "    ensures fresh(Repr - {this});") "" +

+      (__PrintPrePost (newline + "    ensures ") postExpr) + 

+      newline +

       "  {" + newline + 

       body + 

       "  }" + newline

   | _ -> ""

 

-// solutions: (comp, constructor) |--> (heap, env, ctx) 

-let PrintImplCode prog solutions methodsToPrintFunc =

+// solutions: (comp, constructor) |--> condition * heapInst

+let PrintImplCode prog solutions methodsToPrintFunc genRepr =

   let methods = methodsToPrintFunc prog

   PrintDafnyCodeSkeleton prog (fun comp mthd ->

                                  if Utils.ListContains (comp,mthd) methods  then

                                    let mthdBody = match Map.tryFind (comp,mthd) solutions with

-                                                  | Some(sol) -> PrintHeapCreationCode sol 4

+                                                  | Some(sol) -> PrintHeapCreationCode prog sol 4 genRepr

                                                   | _ -> "    //unable to synthesize" + newline

-                                   (GenConstructorCode mthd mthdBody) + newline

+                                   (GenConstructorCode mthd mthdBody genRepr) + newline

                                  else

-                                   "")
\ No newline at end of file
+                                   "") genRepr
\ No newline at end of file
diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index 4b9b0c60..f04a0ca5 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -24,6 +24,15 @@ open AstUtils
 open Utils

 

 open Microsoft.Boogie

+

+type HeapModel = {

+   heap : Map<Const * VarDecl, Const>; 

+   env  : Map<Const, Const>; 

+   ctx  : Set<Set<Const>>;

+}

+

+let MkHeapModel heap env ctx = 

+  { heap = heap; env = env; ctx = ctx }

                                          

 let GetElemFullName (elem: Model.Element) = 

   elem.Names |> Seq.filter (fun ft -> ft.Func.Arity = 0)

@@ -140,7 +149,11 @@ let ReadHeap (model: Microsoft.Boogie.Model) prog =
                         let clsName = if dotIdx = -1 then "" else fldFullName.Substring(0, dotIdx)

                         let refVal = ft.Result

                         let refObj = Unresolved(GetRefName ref)

-                        let fldVarOpt = FindVar prog clsName fldName

+                        let nonebuilder = CascadingBuilder<_>(None)

+                        let fldVarOpt = nonebuilder {

+                          let! comp = FindComponent prog clsName

+                          return FindVar comp fldName

+                        }

                         match fldVarOpt with

                         | Some(fldVar) ->

                             let fldType = match fldVar with 

@@ -165,7 +178,7 @@ let rec ReadArgValues (model: Microsoft.Boogie.Model) args =
           assert (Seq.length func.Apps = 1)

           let ft = Seq.head func.Apps

           let fldVal = ConvertValue model (ft.Result)

-          ReadArgValues model rest |> Map.add (Unresolved(name)) fldVal

+          ReadArgValues model rest |> Map.add (VarConst(name)) fldVal

       | None -> failwith ("cannot find corresponding function for parameter " + name)

   | [] -> Map.empty

 

@@ -382,4 +395,4 @@ let ReadFieldValuesFromModel (model: Microsoft.Boogie.Model) prog comp meth =
   let heap = ReadHeap model prog

   let env0,ctx = ReadEnv model prog

   let env = env0 |> Utils.MapAddAll (ReadArgValues model (GetMethodArgs meth))

-  heap,env,ctx
\ No newline at end of file
+  MkHeapModel heap env ctx
\ No newline at end of file
diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index d1dc73fc..86974f20 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -1,6 +1,7 @@
 module DafnyPrinter
 
 open Ast
+open AstUtils
 open Printer
 
 let rec PrintType ty =
@@ -56,7 +57,6 @@ let rec PrintConst cst =
   | NullConst          -> "null"
   | NoneConst          -> "<none>"
   | ThisConst(_,_)     -> "this"
-  | ExprConst(e)       -> PrintExpr 0 e
   | NewObj(name,_)     -> PrintGenSym name
   | Unresolved(name)   -> sprintf "Unresolved(%s)" name
 
@@ -69,4 +69,15 @@ let PrintFields vars indent ghost =
   let ghostStr = if ghost then "ghost " else ""
   vars |> List.fold (fun acc v -> match v with 
                                   | Var(nm,None)     -> acc + (sprintf "%s%svar %s;%s" (Indent indent) ghostStr nm newline)
-                                  | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""
\ No newline at end of file
+                                  | Var(nm,Some(tp)) -> acc + (sprintf "%s%svar %s: %s;%s" (Indent indent) ghostStr nm (PrintType tp) newline)) ""
+
+let rec PrintStmt stmt indent =

+  let idt = (Indent indent)

+  match stmt with

+  | Block(stmts) ->

+      idt + "{" + newline +

+      (PrintStmtList stmts (indent + 2)) +

+      idt + "}" + newline

+  | Assign(lhs,rhs) -> sprintf "%s%s := %s;%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline

+and PrintStmtList stmts indent =

+  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
\ No newline at end of file
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 5e1bea61..8642cb6b 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Number.jen /method:Number.Abs /checkUnifs</StartArguments>

+    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Triple /genRepr /noVerifyParSol</StartArguments>

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs
index a03f7213..4bd59b11 100644
--- a/Jennisys/Options.fs
+++ b/Jennisys/Options.fs
@@ -11,19 +11,27 @@ open Utils
 type Config = {

    inputFilename: string;

    methodToSynth: string;

+   verifyPartialSolutions: bool;

    verifySolutions: bool;

    checkUnifications: bool;

+   genRepr: bool;

    timeout: int;

+   numLoopUnrolls: int;

 }

 

 let defaultConfig: Config = {

   inputFilename     = "";

   methodToSynth     = "*";

+  verifyPartialSolutions = true;

   verifySolutions   = true;

   checkUnifications = false;

+  genRepr           = false;

   timeout           = 0;

+  numLoopUnrolls    = 2;

 }

 

+/// Should not be mutated outside the ParseCmdLineArgs method, which is 

+/// typically called only once at the beginning of the program execution 

 let mutable CONFIG = defaultConfig

 

 exception InvalidCmdLineArg of string

@@ -78,6 +86,12 @@ let ParseCmdLineArgs args =
         | "method"    -> 

             __CheckNonEmpty value opt

             __Parse rest { cfg with methodToSynth = value }

+        | "verifyParSol" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with verifyPartialSolutions = b }

+        | "noVerifyParSol" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with verifyPartialSolutions = not b }

         | "verifySol" -> 

             let b = __CheckBool value opt

             __Parse rest { cfg with verifySolutions = b }

@@ -90,24 +104,24 @@ let ParseCmdLineArgs args =
         | "noCheckUnifs" -> 

             let b = __CheckBool value opt

             __Parse rest { cfg with checkUnifications = not b }

+        | "genRepr" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with genRepr = b }

+        | "noGenRepr" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with genRepr = not b }

         | "timeout" ->

             let t = __CheckInt value opt

             __Parse rest { cfg with timeout = t }

+        | "unrolls" ->

+            let t = __CheckInt value opt

+            __Parse rest { cfg with numLoopUnrolls = t }

         | "" -> 

             __Parse rest { cfg with inputFilename = value }

         | _ -> 

             raise (InvalidCmdLineOption("Unknown option: " + opt))

     | [] -> cfg   

     

-  let __CheckBool value optName =

-    if value = "" then

-      true

-    else

-      try 

-        System.Boolean.Parse value

-      with 

-        | ex -> raise (InvalidCmdLineArg("Option " + optName " must be boolean"))

-

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

   CONFIG <- __Parse args defaultConfig

 

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index e051492f..f8f2933b 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -1,138 +1,134 @@
-module Printer
-
-open Ast
-open AstUtils
-
-let newline = System.Environment.NewLine // "\r\n"
-
-let PrintGenSym name =
-  sprintf "gensym%s" name
-
-let rec PrintSep sep f list =
-  match list with
-  | [] -> ""
-  | [a] -> f a
-  | a :: more -> (f a) + sep + (PrintSep sep f more)
-  
-let rec PrintType ty =
-  match ty with
-  | IntType                   -> "int"
-  | BoolType                  -> "bool"
-  | NamedType(id, args)       -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args)
-  | SeqType(t)                -> sprintf "seq[%s]" (PrintType t)
-  | SetType(t)                -> sprintf "set[%s]" (PrintType t)
-  | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)
-
-let PrintVarDecl vd =
-  match vd with
-  | Var(id,None) -> id
-  | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)
-
-let PrintVarName vd =
-  match vd with
-  | Var(id,_) -> id
-
-let rec PrintExpr ctx expr =
-  match expr with
-  | IntLiteral(d)     -> sprintf "%d" d
-  | BoolLiteral(b)    -> sprintf "%b" b
-  | ObjLiteral(id)
-  | VarLiteral(id) 
-  | IdLiteral(id)     -> id
-  | Star              -> "*"
-  | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id
-  | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))
-  | UnaryExpr(op,e)   -> sprintf "%s%s" op (PrintExpr 90 e)
-  | BinaryExpr(strength,op,e0,e1) ->
-      let needParens = strength <= ctx
-      let openParen = if needParens then "(" else ""
-      let closeParen = if needParens then ")" else ""
-      sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
-  | IteExpr(c,e1,e2)  -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
-  | SelectExpr(e,i)   -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) 
-  | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
-  | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0))
-  | SeqLength(e)      -> sprintf "|%s|" (PrintExpr 0 e)
-  | SetExpr(ee)       -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0))
-  | ForallExpr(vv,e)  ->
-      let needParens = ctx <> 0
-      let openParen = if needParens then "(" else ""
-      let closeParen = if needParens then ")" else ""
-      sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen
-
-let rec PrintConst cst = 
-  match cst with 
-  | IntConst(v)        -> sprintf "%d" v
-  | BoolConst(b)       -> sprintf "%b" b
-  | VarConst(v)        -> sprintf "%s" v
-  | SetConst(cset)     -> sprintf "{%s}" (PrintSep " " (fun c -> PrintConst c) (Set.toList cset))
-  | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep " " (fun c -> PrintConst c) cseq)
-  | NullConst          -> "null"
-  | NoneConst          -> "<none>"
-  | ThisConst(_,_)     -> "this"
-  | ExprConst(e)       -> PrintExpr 0 e
-  | NewObj(name,_)     -> PrintGenSym name
-  | Unresolved(name)   -> sprintf "Unresolved(%s)" name
-
-let PrintSig signature =
-  match signature with
-  | Sig(ins, outs) ->
-      let returnClause = 
-        if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl)
-        else ""
-      sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause
-
-let rec Indent i =
-  if i = 0 then "" else " " + (Indent (i-1))
-
-let rec PrintStmt stmt indent =
-  let idt = (Indent indent)
-  match stmt with
-  | Block(stmts) ->
-      idt + "{" + newline +
-      (PrintStmtList stmts (indent + 2)) +
-      idt + "}" + newline
-  | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline
-and PrintStmtList stmts indent =
-  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""
-
-let PrintRoutine signature pre body =
-  let preStr = pre |> ForeachConjunct (fun e -> sprintf "    requires %s%s" (PrintExpr 0 e) newline)
-  sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body)  
-  
-let PrintMember m =
-  match m with
-  | Field(vd) -> sprintf "  var %s%s" (PrintVarDecl vd) newline 
-  | Method(id,signature,pre,body,true) -> sprintf "  constructor %s%s" id (PrintRoutine signature pre body)
-  | Method(id,signature,pre,body,false) -> sprintf "  method %s%s" id (PrintRoutine signature pre body)
-  | Invariant(_) -> ""  // invariants are handled separately
-      
-let PrintTopLevelDeclHeader kind id typeParams =
-  let typeParamStr = 
-    match typeParams with
-    | [] -> ""
-    | _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp))
-  sprintf "%s %s%s {%s" kind id typeParamStr newline
-  
-let PrintDecl d =
-  match d with
-  | Class(id,typeParams,members) ->
-      sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams)
-                        (List.fold (fun acc m -> acc + (PrintMember m)) "" members)
-                        newline
-  | Model(id,typeParams,vars,frame,inv) ->
-      (PrintTopLevelDeclHeader "model" id typeParams) + 
-      (vars |> List.fold (fun acc vd -> acc + "  var " + (PrintVarDecl vd) + newline) "") +
-      "  frame" + newline +
-      (frame |> List.fold (fun acc fr -> acc + "    " + (PrintExpr 0 fr) + newline) "") +
-      "  invariant" + newline + 
-      (inv |> ForeachConjunct (fun e -> "    " + (PrintExpr 0 e) + newline)) +
-      "}" + newline
-  | Code(id,typeParams) ->
-      (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline
-
-let PrintMethodSignFull indent m = 
-  let idt = Indent indent
+module Printer

+

+open Ast

+open AstUtils

+

+let newline = System.Environment.NewLine // "\r\n"

+

+let rec PrintSep sep f list =

+  match list with

+  | [] -> ""

+  | [a] -> f a

+  | a :: more -> (f a) + sep + (PrintSep sep f more)

+  

+let rec PrintType ty =

+  match ty with

+  | IntType                   -> "int"

+  | BoolType                  -> "bool"

+  | NamedType(id, args)       -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args)

+  | SeqType(t)                -> sprintf "seq[%s]" (PrintType t)

+  | SetType(t)                -> sprintf "set[%s]" (PrintType t)

+  | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)

+

+let PrintVarDecl vd =

+  match vd with

+  | Var(id,None) -> id

+  | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

+

+let PrintVarName vd =

+  match vd with

+  | Var(id,_) -> id

+

+let rec PrintExpr ctx expr =

+  match expr with

+  | IntLiteral(d)     -> sprintf "%d" d

+  | BoolLiteral(b)    -> sprintf "%b" b

+  | ObjLiteral(id)

+  | VarLiteral(id) 

+  | IdLiteral(id)     -> id

+  | Star              -> "*"

+  | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id

+  | UnaryExpr(op,UnaryExpr(op2, e2))   -> sprintf "%s(%s)" op (PrintExpr 90 (UnaryExpr(op2, e2)))

+  | UnaryExpr(op,e)   -> sprintf "%s%s" op (PrintExpr 90 e)

+  | BinaryExpr(strength,op,e0,e1) ->

+      let needParens = strength <= ctx

+      let openParen = if needParens then "(" else ""

+      let closeParen = if needParens then ")" else ""

+      sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen

+  | IteExpr(c,e1,e2)  -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)

+  | SelectExpr(e,i)   -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) 

+  | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)

+  | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0))

+  | SeqLength(e)      -> sprintf "|%s|" (PrintExpr 0 e)

+  | SetExpr(ee)       -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0))

+  | ForallExpr(vv,e)  ->

+      let needParens = ctx <> 0

+      let openParen = if needParens then "(" else ""

+      let closeParen = if needParens then ")" else ""

+      sprintf "%sforall %s :: %s%s" openParen (vv |> PrintSep ", " PrintVarDecl) (PrintExpr 0 e) closeParen

+

+let rec PrintConst cst = 

+  match cst with 

+  | IntConst(v)        -> sprintf "%d" v

+  | BoolConst(b)       -> sprintf "%b" b

+  | VarConst(v)        -> sprintf "%s" v

+  | SetConst(cset)     -> sprintf "{%s}" (PrintSep " " (fun c -> PrintConst c) (Set.toList cset))

+  | SeqConst(cseq)     -> sprintf "[%s]" (PrintSep " " (fun c -> PrintConst c) cseq)

+  | NullConst          -> "null"

+  | NoneConst          -> "<none>"

+  | ThisConst(_,_)     -> "this"

+  | NewObj(name,_)     -> PrintGenSym name

+  | Unresolved(name)   -> sprintf "Unresolved(%s)" name

+

+let PrintSig signature =

+  match signature with

+  | Sig(ins, outs) ->

+      let returnClause = 

+        if outs <> [] then sprintf " returns (%s)" (outs |> PrintSep ", " PrintVarDecl)

+        else ""

+      sprintf "(%s)%s" (ins |> PrintSep ", " PrintVarDecl) returnClause

+

+let rec Indent i =

+  if i = 0 then "" else " " + (Indent (i-1))

+

+let rec PrintStmt stmt indent =

+  let idt = (Indent indent)

+  match stmt with

+  | Block(stmts) ->

+      idt + "{" + newline +

+      (PrintStmtList stmts (indent + 2)) +

+      idt + "}" + newline

+  | Assign(lhs,rhs) -> sprintf "%s%s := %s%s" idt (PrintExpr 0 lhs) (PrintExpr 0 rhs) newline

+and PrintStmtList stmts indent =

+  stmts |> List.fold (fun acc s -> acc + (PrintStmt s indent)) ""

+

+let PrintRoutine signature pre body =

+  let preStr = pre |> ForeachConjunct (fun e -> sprintf "    requires %s%s" (PrintExpr 0 e) newline)

+  sprintf "%s%s%s%s" (PrintSig signature) newline preStr (PrintExpr 0 body)  

+  

+let PrintMember m =

+  match m with

+  | Field(vd) -> sprintf "  var %s%s" (PrintVarDecl vd) newline 

+  | Method(id,signature,pre,body,true) -> sprintf "  constructor %s%s" id (PrintRoutine signature pre body)

+  | Method(id,signature,pre,body,false) -> sprintf "  method %s%s" id (PrintRoutine signature pre body)

+  | Invariant(_) -> ""  // invariants are handled separately

+      

+let PrintTopLevelDeclHeader kind id typeParams =

+  let typeParamStr = 

+    match typeParams with

+    | [] -> ""

+    | _ -> sprintf "[%s]" (typeParams |> PrintSep ", " (fun tp -> tp))

+  sprintf "%s %s%s {%s" kind id typeParamStr newline

+  

+let PrintDecl d =

+  match d with

+  | Class(id,typeParams,members) ->

+      sprintf "%s%s}%s" (PrintTopLevelDeclHeader "class" id typeParams)

+                        (List.fold (fun acc m -> acc + (PrintMember m)) "" members)

+                        newline

+  | Model(id,typeParams,vars,frame,inv) ->

+      (PrintTopLevelDeclHeader "model" id typeParams) + 

+      (vars |> List.fold (fun acc vd -> acc + "  var " + (PrintVarDecl vd) + newline) "") +

+      "  frame" + newline +

+      (frame |> List.fold (fun acc fr -> acc + "    " + (PrintExpr 0 fr) + newline) "") +

+      "  invariant" + newline + 

+      (inv |> ForeachConjunct (fun e -> "    " + (PrintExpr 0 e) + newline)) +

+      "}" + newline

+  | Code(id,typeParams) ->

+      (PrintTopLevelDeclHeader "code" id typeParams) + "}" + newline

+

+let PrintMethodSignFull indent m = 

+  let idt = Indent indent

   let __PrintPrePost pfix expr = SplitIntoConjunts expr |> PrintSep newline (fun e -> pfix + (PrintExpr 0 e) + ";")

   match m with

   | Method(methodName, sgn, pre, post, isConstr) ->  

@@ -142,9 +138,15 @@ let PrintMethodSignFull indent m =
       idt + mc + " " + methodName + (PrintSig sgn) + newline +

       preStr + (if preStr = "" then "" else newline) +

       postStr

-      
-  | _ -> failwithf "not a method: %O" m
-
-let Print prog =
-  match prog with
-  | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls
+      

+  | _ -> failwithf "not a method: %O" m

+

+let Print prog =

+  match prog with

+  | SProgram(decls) -> List.fold (fun acc d -> acc + (PrintDecl d)) "" decls

+

+let PrintObjRefName o = 

+  match o with

+  | ThisConst(_,_) -> "this";

+  | NewObj(name, _) -> PrintGenSym name

+  | _ -> failwith ("unresolved object ref: " + o.ToString())
\ No newline at end of file
diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index af49e51a..64f80584 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -11,6 +11,15 @@ open Ast
 open AstUtils 

 open Printer

 open EnvUtils

+open DafnyModelUtils

+

+type Obj = { name: string; objType: Type }

+

+type HeapInstance = {

+   assignments: Map<Obj * VarDecl, Expr>; // the first string is the symbolic name of an object literal

+   methodArgs: Map<string, Const>;

+   globals: Map<string, Expr>;

+}

 

 // resolving values

 exception ConstResolveFailed of string

@@ -21,30 +30,35 @@ exception ConstResolveFailed of string
 /// If unable to resolve, it just delegates the task to the

 /// failResolver function

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

-let rec ResolveCont (env,ctx) failResolver cst =

+let rec ResolveCont hModel failResolver cst =

   match cst with

   | Unresolved(_) as u -> 

       // see if it is in the env map first

-      let envVal = Map.tryFind cst env

+      let envVal = Map.tryFind cst hModel.env

       match envVal with

-      | Some(c) -> ResolveCont (env,ctx) failResolver c

+      | Some(c) -> ResolveCont hModel failResolver c

       | None -> 

           // not found in the env map --> check the equality sets

-          let eq = ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)

-                       |> Utils.SetToOption

+          let eq = hModel.ctx |> Set.filter (fun eqSet -> Set.contains u eqSet)

+                              |> Utils.SetToOption

           match eq with 

           | Some(eqSet) -> 

               let cOpt = eqSet |> Set.filter (function Unresolved(_) -> false | _ -> true)

                                |> Utils.SetToOption

               match cOpt with 

               | Some(c) -> c

-              | _ -> failResolver cst (env,ctx)

-          | _ -> failResolver cst (env,ctx)

+              | _ -> failResolver cst hModel

+          | None ->

+              // finally, see if it's a method argument

+              let m = hModel.env |> Map.filter (fun k v -> v = u && match k with VarConst(name) -> true | _ -> false) |> Map.toList

+              match m with 

+              | (vc,_) :: [] -> vc

+              | _ -> failResolver cst hModel

   | SeqConst(cseq) -> 

-      let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont (env,ctx) failResolver c :: acc) []

+      let resolvedLst = cseq |> List.rev |> List.fold (fun acc c -> ResolveCont hModel failResolver c :: acc) []

       SeqConst(resolvedLst)

   | SetConst(cset) ->

-      let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont (env,ctx) failResolver c)) Set.empty

+      let resolvedSet = cset |> Set.fold (fun acc c -> acc |> Set.add (ResolveCont hModel failResolver c)) Set.empty

       SetConst(resolvedSet)

   | _ -> cst

 

@@ -53,39 +67,69 @@ let rec ResolveCont (env,ctx) failResolver cst =
 ///

 /// If unable to resolve, just returns the original Unresolved const.

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

-let TryResolve (env,ctx) cst = 

-  ResolveCont (env,ctx) (fun c (e,x) -> c) cst

+let TryResolve hModel cst = 

+  ResolveCont hModel (fun c _ -> c) cst

 

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

 /// Resolves a given Const (cst) with respect to a given env/ctx. 

 ///

 /// If unable to resolve, raises a ConstResolveFailed exception

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

-let Resolve (env,ctx) cst =

-  ResolveCont (env,ctx) (fun c (e,x) -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst

-   

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

-/// Evaluates a given expression with respect to a given heap/env/ctx       

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

-let Eval (heap,env,ctx) resolveVars expr = 

+let Resolve hModel cst =

+  ResolveCont hModel (fun c _ -> raise (ConstResolveFailed("failed to resolve " + c.ToString()))) cst

+ 

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

+/// Evaluates a given expression with respect to a given heap instance       

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

+let Eval heapInst resolveVars expr = 

   let rec __EvalResolver expr = 

     match expr with

-    | VarLiteral(id) when not resolveVars -> VarConst(id)

-    | ObjLiteral("this") -> GetThisLoc env

-    | ObjLiteral("null") -> NullConst

-    | IdLiteral("this") | IdLiteral("null") -> failwith "should never happen anymore" //TODO

-    | VarLiteral(id)

+    | VarLiteral(id) when not resolveVars -> expr

+    | ObjLiteral("this") | ObjLiteral("null") -> expr

+    | IdLiteral("this")  | IdLiteral("null") -> failwith "should never happen anymore" //TODO

+    | VarLiteral(id) -> 

+        let argValue = heapInst.methodArgs |> Map.tryFind id |> Utils.ExtractOptionMsg ("cannot find value for method parameter " + id)

+        argValue |> Const2Expr

     | IdLiteral(id) ->

-        match TryResolve (env,ctx) (Unresolved(id)) with 

-        | Unresolved(_) -> __EvalResolver (Dot(ObjLiteral("this"), id))

-        | _ as c -> c

+        let globalVal = heapInst.globals |> Map.tryFind id

+        match globalVal with

+        | Some(e) -> e

+        | None -> __EvalResolver (Dot(ObjLiteral("this"), id))

     | Dot(e, str) -> 

         let discr = __EvalResolver e

-        let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList

-        match h2 with

-        | ((_,_),x) :: [] -> x

-        | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" (PrintConst discr) str))

-        | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" (PrintConst discr) str))

+        match discr with

+        | ObjLiteral(objName) -> 

+            let h2 = heapInst.assignments |> Map.filter (fun (o,Var(fldName,_)) v -> o.name = objName && fldName = str) |> Map.toList

+            match h2 with

+            | ((_,_),x) :: [] -> x

+            | _ :: _ -> raise (EvalFailed(sprintf "can't evaluate expression deterministically: %s.%s resolves to multiple locations" objName str))

+            | [] -> raise (EvalFailed(sprintf "can't find value for %s.%s" objName str))  // TODO: what if that value doesn't matter for the solution, and that's why it's not present in the model???

+        | _ -> raise (EvalFailed(sprintf "Dot expression discriminator does not resolve to an object literal but %O" discr))

     | _ -> failwith ("NOT IMPLEMENTED YET: " + (PrintExpr 0 expr))

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

-  EvalSym (fun e -> __EvalResolver e |> Resolve (env,ctx) |> Const2Expr) expr

+  EvalSym (fun e -> __EvalResolver e) expr

+

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

+/// Takes an unresolved model of the heap (HeapModel), resolves all 

+/// references in the model and returns an instance of the heap 

+/// (HeapInstance), where all fields for all objects have explicit 

+/// assignments.

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

+let ResolveModel hModel = 

+  let hmap = hModel.heap |> Map.fold (fun acc (o,f) l ->

+                                        let objName, objType = match Resolve hModel o with

+                                                               | ThisConst(_,t) -> "this", t;

+                                                               | NewObj(name, t) -> PrintGenSym name, t

+                                                               | _ -> failwith ("unresolved object ref: " + o.ToString())

+                                        let objType = objType |> Utils.ExtractOptionMsg "unknown object type"

+                                        let value = TryResolve hModel l |> Const2Expr

+                                        acc |> Map.add ({name = objName; objType = objType}, f) value 

+                                     ) Map.empty

+  let argmap = hModel.env |> Map.fold (fun acc k v -> 

+                                         match k with

+                                         | VarConst(name) -> acc |> Map.add name (Resolve hModel v)

+                                         | _ -> acc

+                                      ) Map.empty 

+  { assignments = hmap; 

+    methodArgs  = argmap; 

+    globals     = Map.empty }
\ No newline at end of file
diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
index 886d5868..8c25726a 100644
--- a/Jennisys/Utils.fs
+++ b/Jennisys/Utils.fs
@@ -135,6 +135,12 @@ let ListReplace oldElem newElem lst =
 let ListContains elem lst = 

   lst |> List.exists (fun e -> e = elem)

 

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

+/// Removes all elements in lst that are equal to "elem"

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

+let ListRemove elem lst = 

+  lst |> List.choose (fun e -> if e = elem then None else Some(e))

+

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

 /// ensures: |ret| = max(|lst| - cnt, 0)

 /// ensures: forall i :: cnt <= i < |lst| ==> ret[i] = lst[i-cnt]

@@ -194,6 +200,25 @@ let rec ListSet idx v lst =
 //  =======================================

 let rec MapAddAll map1 map2 = 

   map2 |> Map.fold (fun acc k v -> acc |> Map.add k v) map1

+

+// -------------------------------------------

+// ------------ algorithms -------------------

+// -------------------------------------------

+

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

+/// Topologically sorts a given list

+///

+/// ensures: |ret| = |lst|

+/// ensures: forall e in lst :: e in ret

+/// ensures: forall i,j :: 0 <= i < j < ==> not (followsFunc ret[j] ret[i])

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

+let rec TopSort followsFunc lst = 

+  match lst with

+  | [] -> []

+  | fs :: [] -> [fs]

+  | fs :: rest -> 

+      let min = rest |> List.fold (fun acc elem -> if followsFunc acc elem then elem else acc) fs

+      min :: TopSort followsFunc (ListRemove min lst)

                                                  

 // -------------------------------------------

 // ------ string active patterns -------------

@@ -221,6 +246,12 @@ let IfDo2 cond func2 (a1,a2) =
   else

     a1,a2 

 

+let Ite cond f1 f2 =

+  if cond then

+    f1

+  else

+    f2

+

 type CascadingBuilder<'a>(failVal: 'a) = 

   member this.Bind(v, f) =

     match v with

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index e7f42ddc..63535a20 100644
--- a/Jennisys/examples/List.jen
+++ b/Jennisys/examples/List.jen
@@ -15,10 +15,10 @@ model List[T] {
   var root: Node[T]
 
   frame
-    root * root.list[*]
+    root
 
   invariant
-    (root = null) ==> (|list| = 0)
+    root = null ==> |list| = 0
     root != null ==> list = root.list
 }
 
@@ -40,7 +40,7 @@ model Node[T] {
   var next: Node[T]
 
   frame 
-    data * next
+    next
 
   invariant
     next = null <==> list = [data]
diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen
index e99cf342..61fad148 100644
--- a/Jennisys/examples/List2.jen
+++ b/Jennisys/examples/List2.jen
@@ -27,7 +27,7 @@ model IntList {
   var root: IntNode
 
   frame
-    root * root.list[*]
+    root
 
   invariant
     root = null <==> |list| = 0
@@ -49,7 +49,7 @@ model IntNode {
   var next: IntNode
 
   frame 
-    data * next
+    next
 
   invariant
     next = null ==> list = [data]
diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen
index acb10ad5..776bd43d 100644
--- a/Jennisys/examples/List3.jen
+++ b/Jennisys/examples/List3.jen
@@ -27,7 +27,7 @@ model IntList {
   var root: IntNode
 
   frame
-    root * root.list[*]
+    root
 
   invariant
     root = null  ==> |list| = 0
@@ -63,7 +63,7 @@ model IntNode {
   var next: IntNode
 
   frame 
-    data * next
+    next
 
   invariant
     next = null  ==> |succ| = 0
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
index 6404bfd6..2142738e 100644
--- a/Jennisys/examples/Set.jen
+++ b/Jennisys/examples/Set.jen
@@ -13,13 +13,14 @@ class Set {
   constructor Double(p: int, q: int)
     requires p != q
     ensures elems = {p q}
+
 }
 
 model Set {
   var root: SetNode
 
   frame
-    root * root.elems[*]
+    root
 
   invariant
     root = null ==> elems = {}
@@ -35,6 +36,10 @@ class SetNode {
   constructor Double(p: int, q: int)
     requires p != q
     ensures elems = {p q}
+
+  constructor Triple(p: int, q: int, r: int)
+    requires p != q && q != r && r != p
+    ensures elems = {p q r}
 }
 
 model SetNode {
@@ -43,7 +48,7 @@ model SetNode {
   var right: SetNode
 
   frame 
-    data * left * right
+    left * right
 
   invariant
     elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})