Jennisys:

 - changed the synthesis of the Valid() function to synthesize both unrolled
   and recursive definition of it, because both are needed in certain cases
 - to make the recursive definition of Valid() work, a "decreases" clause is
   needed.  For now, decreases clause is always "decreases Repr", and that
   seems to be enough for now.

9 files changed, 133 insertions, 75 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index 9dcfb2ae..f439c8d0 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -83,7 +83,7 @@ let rec MethodAnalysisPrinter onlyForThese assertion comp =
 /// path.  It starts from the given object, and follows the backpointers

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

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

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

+// 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 

@@ -100,18 +100,22 @@ let GetObjRefExpr objRefName (heapInst: HeapInstance) =
                 | Some(expr) -> Some(Dot(expr, fldName))

                 | None -> __fff rest

             | [] -> None

-          let backPointers = heapInst.assignments |> List.choose (function FieldAssignment (x,l) -> if l = ObjLiteral(objRefName) then Some(x,l) else None

-                                                                           |_ -> None)

+          let backPointers = heapInst.assignments |> List.choose (function 

+                                                                    FieldAssignment (x,l) -> 

+                                                                      if l = ObjLiteral(objRefName) then Some(x,l) else None

+                                                                    |_ -> None)

           __fff backPointers 

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

-  if objRef2ExprCache.ContainsKey(objRefName) then

-    Some(objRef2ExprCache.[objRefName])

-  else

-    let res = __GetObjRefExpr objRefName (Set.empty)

-    match res with 

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

-    | None -> ()

-    res

+  __GetObjRefExpr objRefName (Set.empty)

+// THIS DOESN'T WORK BECAUSE THE CACHE HAS TO BE PURGED AFTER EVERY METHOD

+//  if objRef2ExprCache.ContainsKey(objRefName) then

+//    Some(objRef2ExprCache.[objRefName])

+//  else

+//    let res = __GetObjRefExpr objRefName (Set.empty)

+//    match res with 

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

+//    | None -> ()

+//    res

 

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

 /// Returns an expression that combines the post-condition of a given method with

@@ -156,6 +160,8 @@ let IsUnmodOnly (comp,meth) expr =
         // let lhsType = InferType prog e

         // let isMod = IsFieldModifiable lhsType fldName

         // (not isMod) && __IsUnmodOnlyLst [e]

+    | AssertExpr(e)

+    | AssumeExpr(e)

     | SeqLength(e)

     | LCIntervalExpr(e)

     | UnaryExpr(_,e)                       -> __IsUnmodOnlyLst [e]

@@ -256,7 +262,7 @@ let rec ApplyUnifications indent prog comp mthd unifs heapInst conservative =
                           | 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) false

+      let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,mthd] assertionExpr) true

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

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

       if ok then

@@ -371,7 +377,7 @@ let rec AnalyzeConstructor indent prog comp m callGraph =
       let methodName = GetMethodName m

       let pre,post = GetMethodPrePost m

       // generate Dafny code for analysis first

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

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

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

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

       if models.Count = 0 then

@@ -415,6 +421,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph =
   let methodArgs = GetMethodInArgs m

   let expr = GetHeapExpr prog m heapInst2

   // now evaluate and see what's left

+  // printf "%s" (expr |> SplitIntoConjunts |> PrintSep newline (fun e -> PrintExpr 0 e))

   let newCond = Eval heapInst2 (DontResolveUnmodifiableStuff prog comp m) expr

   if newCond = TrueLiteral then

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

diff --git a/Jennisys/Jennisys/Ast.fs b/Jennisys/Jennisys/Ast.fs
index cad5352c..beb4ba2e 100644
--- a/Jennisys/Jennisys/Ast.fs
+++ b/Jennisys/Jennisys/Ast.fs
@@ -49,6 +49,8 @@ type Expr =
   | ForallExpr of VarDecl list * Expr

   | MethodCall of (* receiver *) Expr * (* component name *) string * (* method name *) string * (* actual parameters *) Expr list

   | VarDeclExpr of (* var list *) VarDecl list * (* declareAlso *) bool

+  | AssertExpr of Expr

+  | AssumeExpr of Expr

 

 type Const = 

   | IntConst   of int

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index a1f391a9..a866ad08 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -41,6 +41,8 @@ let rec Rewrite rewriterFunc expr =
   | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map __RewriteOrRecurse)

   | SetExpr(exs)                     -> SetExpr(exs |> List.map __RewriteOrRecurse)

   | MethodCall(rcv,cname,mname,ins)  -> MethodCall(__RewriteOrRecurse rcv, cname, mname, ins |> List.map __RewriteOrRecurse)

+  | AssertExpr(e)                    -> AssertExpr(__RewriteOrRecurse e)

+  | AssumeExpr(e)                    -> AssumeExpr(__RewriteOrRecurse e)

 

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

 /// Substitutes all occurences of all IdLiterals having 

@@ -103,6 +105,8 @@ let rec DescendExpr visitorFunc composeFunc leafVal expr =
   | ObjLiteral(_)                      

   | VarDeclExpr(_)

   | IdLiteral(_)                     -> leafVal

+  | AssertExpr(e)

+  | AssumeExpr(e)

   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

@@ -128,6 +132,8 @@ let rec DescendExpr2 visitorFunc expr acc =
   | ObjLiteral(_)   

   | VarDeclExpr(_)                   

   | IdLiteral(_)                     -> newAcc

+  | AssertExpr(e)

+  | AssumeExpr(e)

   | Dot(e, _)

   | ForallExpr(_,e)

   | LCIntervalExpr(e)

@@ -582,6 +588,8 @@ let rec __EvalSym resolverFunc ctx expr =
   | ObjLiteral(_)  -> expr

   | Star           -> expr //TODO: can we do better?

   | VarDeclExpr(_) -> expr

+  | AssertExpr(e)  -> AssertExpr(__EvalSym resolverFunc ctx e)

+  | AssumeExpr(e)  -> AssumeExpr(__EvalSym resolverFunc ctx e)

   | VarLiteral(id) -> 

       try 

         let _,e = ctx |> List.find (fun (v,e) -> GetVarName v = id)

@@ -854,6 +862,8 @@ let MyDesugar expr removeOriginal =
     | ForallExpr(v,e)        -> ForallExpr(v, __Desugar e)

     | LCIntervalExpr(e)      -> LCIntervalExpr(__Desugar e)

     | UnaryExpr(op,e)        -> UnaryExpr(op, __Desugar e)

+    | AssertExpr(e)          -> AssertExpr(__Desugar e)

+    | AssumeExpr(e)          -> AssumeExpr(__Desugar e)

     | IteExpr(c,e1,e2)       -> IteExpr(c, __Desugar e1, __Desugar e2)

     // lst = [a1 a2 ... an] ~~~> lst = [a1 a2 ... an] && lst[0] = a1 && lst[1] = a2 && ... && lst[n-1] = an && |lst| = n

     | BinaryExpr(p,op,e1,e2) -> 

@@ -906,6 +916,8 @@ let ChangeThisReceiver receiver expr =
     | IdLiteral("this")                    -> failwith "should never happen anymore"

     | IdLiteral(id)                        -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(ObjLiteral("this"), id))

     | Dot(e, id)                           -> Dot(__ChangeThis locals e, id)

+    | AssertExpr(e)                        -> AssertExpr(__ChangeThis locals e)

+    | AssumeExpr(e)                        -> AssumeExpr(__ChangeThis locals e)

     | ForallExpr(vars,e)                   -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

                                               ForallExpr(vars, __ChangeThis newLocals e)   

     | LCIntervalExpr(e)                    -> LCIntervalExpr(__ChangeThis locals e)

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 8414c8ce..a6caaa6e 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -9,18 +9,13 @@ open PrintUtils
 open DafnyPrinter

 open DafnyModelUtils

 

-// 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

-//  else

-//    BinaryImplies (BinaryNeq fldExpr (ObjLiteral("null")))

-//                  (BinaryAnd (Dot(fldExpr, validFunName))

-//                             (GetUnrolledFieldValidExpr (Dot(fldExpr, fldName)) fldName validFunName (numUnrolls-1)))

+let validFuncName = "Valid()"

+let validSelfFuncName = "Valid_self()"

+let validReprFuncName = "Valid_repr()"

 

 /// requires: numUnrols >= 0

 /// requires: |fldExprs| = |fldNames|

-let rec GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls = 

+let rec GetUnrolledFieldValidExpr fldExprs fldNames validFuncToUse numUnrolls = 

   let rec __Combine exprLst strLst = 

     match exprLst with

     | e :: rest ->

@@ -38,21 +33,24 @@ let rec GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls =
   if numUnrolls = 0 then

     [TrueLiteral]

   else

-    let exprList = fldExprs |> List.map (fun e -> BinaryImplies (__NotNull e) (Dot(e, validFunName)))

+    let exprList = fldExprs |> List.map (fun e -> BinaryImplies (__NotNull e) (Dot(e, validFuncToUse)))

     if numUnrolls = 1 then 

       exprList

     else 

       let fldExprs = __Combine fldExprs fldNames

-      List.append exprList (GetUnrolledFieldValidExpr fldExprs fldNames validFunName (numUnrolls - 1))

-                                                                    

-

-//let GetFieldValidExpr fldName validFunName numUnrolls : Expr = 

-//  GetUnrolledFieldValidExpr (IdLiteral(fldName)) fldName validFunName numUnrolls

-

+      List.append exprList (GetUnrolledFieldValidExpr fldExprs fldNames validFuncToUse (numUnrolls - 1))

+                                  

 let GetFieldValidExpr flds validFunName numUnrolls = 

   let fldExprs = flds |> List.map (function Var(name, _) -> IdLiteral(name))

   let fldNames = flds |> List.map (function Var(name, _) -> name)

-  GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls

+  let unrolledExprs = GetUnrolledFieldValidExpr fldExprs fldNames validFunName numUnrolls

+  // add the recursive definition as well

+  let recExprs = 

+    if not (validFunName = validFuncName) && Options.CONFIG.recursiveValid then

+      flds |> List.map (function Var(name,_) -> BinaryImplies (BinaryNeq (IdLiteral(name)) NullLiteral) (Dot(IdLiteral(name), validFuncName)))

+    else

+      []

+  recExprs @ unrolledExprs

 

 let GetFieldsForValidExpr allFields prog : VarDecl list =

   allFields |> List.filter (function Var(name, tp) when IsUserType prog tp -> true

@@ -64,19 +62,11 @@ let GetFieldsValidExprList clsName allFields prog : Expr list =
   fieldsByType |> Map.fold (fun acc t varSet ->

                               let validFunName, numUnrolls = 

                                 match t with

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

-                                | _ -> "Valid()", 1 

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

+                                | _ -> validFuncName, 1 

                               acc |> List.append (GetFieldValidExpr (Set.toList varSet) validFunName numUnrolls)

                            ) []

 

-//  fields |> List.map (function Var(name, t) -> 

-//                                 let validFunName, numUnrolls = 

-//                                   match t with

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

-//                                   | _ -> "Valid()", 1

-//                                 GetFieldValidExpr name validFunName numUnrolls

-//                     )

-

 let PrintValidFunctionCode comp prog genRepr: string = 

   let idt = "    "

   let __PrintInvs invs = 

@@ -85,6 +75,8 @@ let PrintValidFunctionCode comp prog genRepr: string =
          |> fun s -> if s = "" then (idt + "true") else s

   let clsName = GetClassName comp

   let vars = GetAllFields comp

+  let compTypeName = GetClassType comp |> PrintType

+  let hasLoop = vars |> List.exists (function Var(_,tyOpt) -> match tyOpt with Some(ty) when compTypeName = PrintType ty -> true | _ -> false)

   let allInvs = GetInvariantsAsList comp |> DesugarLst

   let fieldsValid = GetFieldsValidExprList clsName vars prog

   

@@ -96,31 +88,38 @@ let PrintValidFunctionCode comp prog genRepr: string =
 

   let vr = 

     if genRepr then

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

+      "  function " + validReprFuncName + ": 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) +

+      ""         

+

+  let decreasesStr = 

+    if Options.CONFIG.recursiveValid then 

+      if hasLoop then

+        if genRepr then 

+          "    decreases Repr;" + newline 

+        else 

+          // TODO: Dafny currently doesn't accept "decreases *" on methods

+          "    decreases *;" + newline

+      else 

+        ""

+    else ""

   vr + 

-  "  function Valid_self(): bool" + newline +

+  "  function " + validSelfFuncName + ": bool" + newline +

   "    reads *;" + newline +

   "  {" + newline + 

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

+  (if genRepr then "    " + validReprFuncName + " &&" + newline else "") +

   (__PrintInvs allInvs) + newline +

   "  }" + newline +

   newline +

   "  function Valid(): bool" + newline +

   "    reads *;" + newline +

+  decreasesStr + 

   "  {" + newline + 

-  "    this.Valid_self() &&" + newline +

+  "    this." + validSelfFuncName + " &&" + newline +

   (__PrintInvs fieldsValid) + newline +

   "  }" + newline

 

@@ -145,8 +144,7 @@ let PrintDafnyCodeSkeleton prog methodPrinterFunc genRepr =
         "}" + newline + newline

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

 

-let PrintAllocNewObjects heapInst indent = 

-  let idt = Indent indent

+let GetAllocObjects heapInst = 

   heapInst.assignments |> List.fold (fun acc a ->

                                        match a with

                                        | FieldAssignment((obj,fld),_) when not (obj.name = "this") ->

@@ -155,7 +153,10 @@ let PrintAllocNewObjects heapInst indent =
                                            acc |> Set.add (heapInst.objs |> Map.find name)

                                        | _ -> acc

                                    ) Set.empty

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

+

+let PrintAllocNewObjects heapInst indent = 

+  let idt = Indent indent

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

 

 let PrintVarAssignments heapInst indent = 

   let idt = Indent indent

@@ -215,12 +216,24 @@ let PrintReprAssignments prog heapInst indent =
                                           let fullReprExpr = BinaryGets (Dot(ObjLiteral(obj.name), "Repr")) fullRhs 

                                           fullReprExpr :: acc

                                         ) []

+  let reprValidExpr = GetAllocObjects heapInst |> Set.fold (fun acc obj -> BinaryAnd acc (Dot(ObjLiteral(obj.name), validFuncName))) TrueLiteral

   

-  if not (reprGetsList = []) then

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

-    (PrintStmtList reprGetsList indent true)

-  else

-    ""

+  let reprStr = if not (reprGetsList = []) then

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

+                  (PrintStmtList reprGetsList indent true)

+                else

+                  ""

+

+  let assertValidStr = if not (reprValidExpr = TrueLiteral) then

+                         idt + "// assert repr objects are valid (helps verification)" + newline +

+                         (PrintStmt (ExprStmt(AssertExpr(reprValidExpr))) indent true)

+                       else

+                         ""

+  let outStr = reprStr + assertValidStr     

+  if outStr = "" then

+    outStr

+  else 

+    newline + outStr   

                                                           

 let rec PrintHeapCreationCode prog sol indent genRepr =

   /// just removes all FieldAssignments to unmodifiable objects    

@@ -265,8 +278,8 @@ let rec PrintHeapCreationCode prog sol indent genRepr =
 let PrintPrePost pfix expr = 

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

 

-let GetPreconditionForMethod m = 

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

+let GetPreconditionForMethod prog m = 

+  let validExpr = IdLiteral(validFuncName);

   match m with

   | Method(_,_,pre,_,isConstr) ->

       if isConstr then

@@ -275,11 +288,22 @@ let GetPreconditionForMethod m =
         BinaryAnd validExpr pre

   | _ -> failwithf "expected a method, got %O" m     

 

-let GetPostconditionForMethod m genRepr = 

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

+let GetPostconditionForMethod prog m genRepr = 

+  let validExpr = IdLiteral(validFuncName);

   match m with

   | Method(_,_,_,post,isConstr) ->

+      // this.Valid() and user-defined post-condition

       let postExpr = BinaryAnd validExpr post

+      // method out args are valid

+      let postExpr = (GetMethodOutArgs m) |> List.fold (fun acc (Var(name,tyOpt)) ->

+                                                          if IsUserType prog tyOpt then

+                                                            let varExpr = VarLiteral(name)

+                                                            let argValidExpr = BinaryImplies (BinaryNeq varExpr NullLiteral) (Dot(varExpr, validFuncName))

+                                                            BinaryAnd acc argValidExpr

+                                                          else 

+                                                            acc

+                                                       ) postExpr

+      // fresh Repr

       if genRepr then

         let freshExpr = if isConstr then "fresh(Repr - {this})" else "fresh(Repr - old(Repr))";

         BinaryAnd (IdLiteral(freshExpr)) postExpr

@@ -287,14 +311,14 @@ let GetPostconditionForMethod m genRepr =
         postExpr

   | _ -> failwithf "expected a method, got %O" m     

       

-let GenConstructorCode mthd body genRepr =

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

+let GenConstructorCode prog mthd body genRepr =

+  let validExpr = IdLiteral(validFuncName);

   match mthd with

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

-      let preExpr = GetPreconditionForMethod mthd |> Desugar

-      let postExpr = GetPostconditionForMethod mthd genRepr |> Desugar

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

-      "    modifies this;" + 

+  | Method(methodName, sign, pre, post, isConstr) -> 

+      let preExpr = GetPreconditionForMethod prog mthd |> Desugar

+      let postExpr = GetPostconditionForMethod prog mthd genRepr |> Desugar

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

+      (if isConstr then newline + "    modifies this;" else "") +

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

       (PrintPrePost (newline + "    ensures ") postExpr) + 

       newline +

@@ -313,10 +337,10 @@ let PrintImplCode prog solutions genRepr =
                                                               match sol with

                                                               | [] -> 

                                                                   "    //unable to synthesize" +

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

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

                                                               | _ -> 

                                                                   PrintHeapCreationCode prog sol 4 genRepr

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

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

                                   

                                                           else

                                                             acc) "") genRepr
\ No newline at end of file
diff --git a/Jennisys/Jennisys/DafnyPrinter.fs b/Jennisys/Jennisys/DafnyPrinter.fs
index df20fc4b..947a72f2 100644
--- a/Jennisys/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/Jennisys/DafnyPrinter.fs
@@ -11,7 +11,7 @@ let rec PrintType ty =
   | SeqType(t)                -> sprintf "seq<%s>" (PrintType t)

   | SetType(t)                -> sprintf "set<%s>" (PrintType t)

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

-  | InstantiatedType(id,args) -> sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)

+  | InstantiatedType(id,args) -> if List.isEmpty args then id else sprintf "%s<%s>" id (PrintSep ", " (fun t -> PrintType t) args)

 

 let PrintVarDecl vd =

   match vd with

@@ -60,6 +60,8 @@ let rec PrintExpr ctx expr =
   | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))

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

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

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

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

   | ForallExpr(vv,e)  ->

       let needParens = true

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

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index b18131de..a3c92ab7 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/List.jen /genRepr  /genMod /method:Node.Tail</StartArguments>

+    <StartArguments>examples/Set.jen /genMod /genRepr /method:Set.Double</StartArguments>

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

   </PropertyGroup>

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

diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs
index feb541a4..b61c16da 100644
--- a/Jennisys/Jennisys/Options.fs
+++ b/Jennisys/Jennisys/Options.fs
@@ -20,6 +20,7 @@ type Config = {
    genMod: bool;

    timeout: int;

    numLoopUnrolls: int;

+   recursiveValid: bool;

 }

 

 type CfgOption<'a> = {

@@ -67,6 +68,8 @@ let cfgOptions = [
   { optionName = "noGenMod";        optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genMod                 = not (CheckBool v "noGenMod")});      descr = "description not available"; }

   { optionName = "timeout";         optionType = "int";    optionSetter = (fun v (cfg: Config) -> {cfg with timeout                =      CheckInt v "timeout"});         descr = "description not available"; }

   { optionName = "unrolls";         optionType = "int";    optionSetter = (fun v (cfg: Config) -> {cfg with numLoopUnrolls         =      CheckInt v "unrolls"});         descr = "description not available"; }

+  { optionName = "recValid";        optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid         =      CheckBool v "recValid"});       descr = "description not available"; }

+  { optionName = "noRecValid";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid         = not (CheckBool v "noRecValid")});    descr = "description not available"; }

 ]

 

 let cfgOptMap = cfgOptions |> List.fold (fun acc o -> acc |> Map.add o.optionName o) Map.empty

@@ -98,10 +101,11 @@ let defaultConfig: Config = {
   verifyPartialSolutions = true;

   verifySolutions   = true;

   checkUnifications = false;

-  genRepr           = false;

+  genRepr           = true;

   genMod            = false;

   timeout           = 0;

   numLoopUnrolls    = 2;

+  recursiveValid    = true;

 }

 

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

diff --git a/Jennisys/Jennisys/Printer.fs b/Jennisys/Jennisys/Printer.fs
index 95638ea5..7de4c27d 100644
--- a/Jennisys/Jennisys/Printer.fs
+++ b/Jennisys/Jennisys/Printer.fs
@@ -46,6 +46,8 @@ let rec PrintExpr ctx expr =
   | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0))

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

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

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

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

   | ForallExpr(vv,e)  ->

       let needParens = ctx <> 0

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

diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
index ca21b65b..bb36c2bb 100644
--- a/Jennisys/Jennisys/examples/List.jen
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -41,6 +41,11 @@ class Node[T] {
   method Tail() returns (tail: Node[T])
     ensures |list| = 1 ==> tail = null
     ensures |list| > 1 ==> tail != null && tail.list = list[1..]
+
+  method SkipFew(num: int) returns (ret: Node[T])
+    requires num >= 0
+    ensures num >= |list| ==> ret = null
+    ensures num < |list| ==> ret != null && ret.list = list[num..]
 }
 
 model Node[T] {