- updated the examples to use the new keywords (interface/datamodel)

 - updated the README.txt file with instructions on how to run examples
 - added descriptions for command-line switches
 - changed genMod option to be true by default

8 files changed, 54 insertions, 41 deletions

diff --git a/Jennisys/Jennisys/Options.fs b/Jennisys/Jennisys/Options.fs
index 255e7ecf..2be3a550 100644
--- a/Jennisys/Jennisys/Options.fs
+++ b/Jennisys/Jennisys/Options.fs
@@ -34,7 +34,7 @@ type CfgOption<'a> = {
 

 exception InvalidCmdLineArg of string

 exception InvalidCmdLineOption of string

-

+ 

 let CheckNonEmpty value optName =

   if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty")) else value

 

@@ -54,25 +54,25 @@ let CheckBool value optName =
       | ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer"))

 

 let cfgOptions = [

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

-  { optionName = "method";          optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth          = CheckNonEmpty v "method"});          descr = "description not available"; }

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

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

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

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

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

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

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

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

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

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

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

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

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

+  { optionName = "help";            optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with help                   =      CheckBool v "help"});           descr = "prints out the available switches"; }

+  { optionName = "method";          optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth          = CheckNonEmpty v "method"});          descr = "select methods to synthesize; method names are in the form <ClassName>.<MethodName>; multiple methods can be given as a list of comma separated values"; }

+  { optionName = "constrOnly";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with constructorsOnly       =      CheckBool v "constrOnly"});     descr = "synthesize constructors only"; }

+  { optionName = "inferConds";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals      =      CheckBool v "inferConds"});     descr = "try to infer conditions"; }

+  { optionName = "noInferConds";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals      = not (CheckBool v "inferConds")});    descr = "don't try to infer conditions"; }

+  { optionName = "verifyParSol";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions =      CheckBool v "verifyParSol"});   descr = "verify partial solutions"; }

+  { optionName = "noVerifyParSol";  optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = not (CheckBool v "verifyParSol")});  descr = "don't verify partial solutions"; }

+  { optionName = "verifySol";       optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions        =      CheckBool v "verifySol"});      descr = "verify final solution"; }

+  { optionName = "noVerifySol";     optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions        = not (CheckBool v "verifySol")});     descr = "don't verify final solution"; } 

+  { optionName = "checkUnifs";      optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications      =      CheckBool v "checkUnifs"});     descr = "verify unifications"; } 

+  { optionName = "noCheckUnifs";    optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications      = not (CheckBool v "noCheckUnifs")});  descr = "don't verify unifications"; }

+  { optionName = "genRepr";         optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genRepr                =      CheckBool v "genRepr"});        descr = "generate Repr field"; }

+  { optionName = "noGenRepr";       optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genRepr                = not (CheckBool v "noGenRepr")});     descr = "don't generate Repr field"; }

+  { optionName = "genMod";          optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genMod                 =      CheckBool v "genMod"});         descr = "generate modular code (delegate to methods)"; }

+  { optionName = "noGenMod";        optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with genMod                 = not (CheckBool v "noGenMod")});      descr = "dont generate modular code (delegate to methods)"; }

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

+  { optionName = "unrolls";         optionType = "int";    optionSetter = (fun v (cfg: Config) -> {cfg with numLoopUnrolls         =      CheckInt v "unrolls"});         descr = "number of unrolls of the Valid() function"; }

+  { optionName = "recValid";        optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid         =      CheckBool v "recValid"});       descr = "generate recursive Valid() function"; }

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

   { optionName = "break";           optionType = "bool";   optionSetter = (fun v (cfg: Config) -> {cfg with breakIntoDebugger      =      CheckBool v "break"});          descr = "launches debugger upon start-up"; }

 ]

 

@@ -107,7 +107,7 @@ let defaultConfig: Config = {
   verifySolutions   = true;

   checkUnifications = false;

   genRepr           = true;

-  genMod            = false;

+  genMod            = true;

   timeout           = 0;

   numLoopUnrolls    = 2;

   recursiveValid    = true;

diff --git a/Jennisys/Jennisys/README.txt b/Jennisys/Jennisys/README.txt
index 0e52dec9..41bb9964 100644
--- a/Jennisys/Jennisys/README.txt
+++ b/Jennisys/Jennisys/README.txt
@@ -3,3 +3,16 @@
 
   - create c:\tmp folder
   - copy the Jennisys\scripts\StartDafny-jen.bat script into c:\tmp
+
+2. Running the examples
+----------------------------
+
+  $ cd Jennisys
+  $ bin/Debug/Jennisys.exe examples/<name>.jen /genRepr /genMod
+
+  /genRepr - generate Repr field 
+  /genMod  - generate modular code (delegate to methods)
+
+  Currenty, in the List.jen example, methods SkipFew and Index cannot
+  be synthesized.  All other methods in List.jen, List2.jen, List3.jen, 
+  Set.jen, Number.jen, and NumberMethods.jen should be synthesizable.
diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
index 0d52aab7..9d29aeee 100644
--- a/Jennisys/Jennisys/examples/List.jen
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -1,4 +1,4 @@
-class List[T] {
+interface List[T] {
   var list: seq[T]
 
   constructor Empty()
@@ -11,7 +11,7 @@ class List[T] {
     ensures list = [p q]
 }
 
-model List[T] {
+datamodel List[T] {
   var root: Node[T]
 
   frame
@@ -22,7 +22,7 @@ model List[T] {
     root != null ==> list = root.list
 }
 
-class Node[T] {
+interface Node[T] {
   var list: seq[T]
 
   invariant
@@ -61,7 +61,7 @@ class Node[T] {
     ensures ret = (n in list)
 }
 
-model Node[T] {
+datamodel Node[T] {
   var data: T
   var next: Node[T]
 
diff --git a/Jennisys/Jennisys/examples/List2.jen b/Jennisys/Jennisys/examples/List2.jen
index acca4ddf..ae8a2845 100644
--- a/Jennisys/Jennisys/examples/List2.jen
+++ b/Jennisys/Jennisys/examples/List2.jen
@@ -1,4 +1,4 @@
-class IntList {
+interface IntList {
   var list: seq[int]
 
   constructor Empty()
@@ -23,7 +23,7 @@ class IntList {
     ensures list = [p + q]
 }
 
-model IntList {
+datamodel IntList {
   var root: IntNode
 
   frame
@@ -34,7 +34,7 @@ model IntList {
     root != null ==> list = root.list
 }
 
-class IntNode {
+interface IntNode {
   var list: seq[int]
 
   invariant
@@ -50,7 +50,7 @@ class IntNode {
     ensures list = [x y]
 }
 
-model IntNode {
+datamodel IntNode {
   var data: int
   var next: IntNode
 
diff --git a/Jennisys/Jennisys/examples/List3.jen b/Jennisys/Jennisys/examples/List3.jen
index 3900b1d1..9130f82a 100644
--- a/Jennisys/Jennisys/examples/List3.jen
+++ b/Jennisys/Jennisys/examples/List3.jen
@@ -1,4 +1,4 @@
-class IntList {
+interface IntList {
   var list: seq[int]
 
   constructor Empty()
@@ -23,7 +23,7 @@ class IntList {
     ensures list = [p + q]
 }
 
-model IntList {
+datamodel IntList {
   var root: IntNode
 
   frame
@@ -36,7 +36,7 @@ model IntList {
                       (forall i :: i in 1 ... |root.succ| ==> (root.succ[i-1] != null && list[i] = root.succ[i-1].data)))
 }
 
-class IntNode {
+interface IntNode {
   var succ: seq[IntNode]
   var data: int
 
@@ -59,7 +59,7 @@ class IntNode {
     !(null in succ)
 }
 
-model IntNode {
+datamodel IntNode {
   var next: IntNode
 
   frame 
diff --git a/Jennisys/Jennisys/examples/Number.jen b/Jennisys/Jennisys/examples/Number.jen
index ce76c09c..e31613bd 100644
--- a/Jennisys/Jennisys/examples/Number.jen
+++ b/Jennisys/Jennisys/examples/Number.jen
@@ -1,4 +1,4 @@
-class Number { 
+interface Number { 
   var num: int
  
   constructor Init(p: int)
@@ -39,6 +39,6 @@ class Number {
 
 }
 
-model Number {
+datamodel Number {
 
 }
\ No newline at end of file
diff --git a/Jennisys/Jennisys/examples/NumberMethods.jen b/Jennisys/Jennisys/examples/NumberMethods.jen
index 91fbc4f9..f9b17f74 100644
--- a/Jennisys/Jennisys/examples/NumberMethods.jen
+++ b/Jennisys/Jennisys/examples/NumberMethods.jen
@@ -1,4 +1,4 @@
-class NumberMethods {
+interface NumberMethods {
  
   method Double(p: int) returns (ret: int)
     ensures ret = 2*p
@@ -35,6 +35,6 @@ class NumberMethods {
 
 }
 
-model NumberMethods {
+datamodel NumberMethods {
 
 }
\ No newline at end of file
diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen
index f87e02f2..a04ee481 100644
--- a/Jennisys/Jennisys/examples/Set.jen
+++ b/Jennisys/Jennisys/examples/Set.jen
@@ -1,4 +1,4 @@
-class Set {
+interface Set {
   var elems: set[int]
 
   constructor Empty()
@@ -19,7 +19,7 @@ class Set {
 
 }
 
-model Set {
+datamodel Set {
   var root: SetNode
 
   frame
@@ -30,7 +30,7 @@ model Set {
     root != null ==> elems = root.elems
 }
 
-class SetNode {
+interface SetNode {
   var elems: set[int]
 
   constructor Init(x: int)
@@ -56,7 +56,7 @@ class SetNode {
     ensures ret = (n in elems)
 }
 
-model SetNode {
+datamodel SetNode {
   var data: int
   var left: SetNode
   var right: SetNode