- 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

6 files changed, 20 insertions, 20 deletions

diff --git a/Jennisys/examples/List.jen b/Jennisys/examples/List.jen
index 0d52aab7..9d29aeee 100644
--- a/Jennisys/examples/List.jen
+++ b/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/examples/List2.jen b/Jennisys/examples/List2.jen
index acca4ddf..ae8a2845 100644
--- a/Jennisys/examples/List2.jen
+++ b/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/examples/List3.jen b/Jennisys/examples/List3.jen
index 3900b1d1..9130f82a 100644
--- a/Jennisys/examples/List3.jen
+++ b/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/examples/Number.jen b/Jennisys/examples/Number.jen
index ce76c09c..e31613bd 100644
--- a/Jennisys/examples/Number.jen
+++ b/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/examples/NumberMethods.jen b/Jennisys/examples/NumberMethods.jen
index 91fbc4f9..f9b17f74 100644
--- a/Jennisys/examples/NumberMethods.jen
+++ b/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/examples/Set.jen b/Jennisys/examples/Set.jen
index f87e02f2..a04ee481 100644
--- a/Jennisys/examples/Set.jen
+++ b/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