Jennisys: Refined parsing of expressions, frames, and routine bodies

3 files changed, 7 insertions, 32 deletions

diff --git a/Test/jennisys0/Answer b/Test/jennisys0/Answer
index 920c87e0..2b7ab098 100644
--- a/Test/jennisys0/Answer
+++ b/Test/jennisys0/Answer
@@ -6,31 +6,25 @@ class C {
   var a: seq[int]

   var x: int

   constructor Init()

-  {

-  }

   method Update(d)

-  {

     x := x + 1

     {

       nested := statement

       yes := sirrie

     }

     x.f := (12 + true)[8000 := 0 <= n]

-  }

   method Query() returns (r)

     requires r

-    requires *

+    requires a[*]

     requires r.r.s

     requires a[i]

     requires a[i := 58]

     requires hello

     requires (hello + goodbye) - soonyousoon

     requires 0 <= r

-  {

-  }

+    {

+    }

   method ManyParams(x: bool, y) returns (r, s: set[MyClass], t)

-  {

-  }

 }

 model C {

   var x: int

@@ -49,25 +43,17 @@ Jennisys, Copyright (c) 2011, Microsoft.
 class ExtensibleArray[T] {

   var Contents: seq[T]

   constructor Init()

-  {

     Contents := []

-  }

   method Get(i) returns (t)

     requires 0 <= i

     requires i < |Contents|

-  {

     t := Contents[i]

-  }

   method Set(i, t)

     requires 0 <= i

     requires i < |Contents|

-  {

     Contents := Contents[i := t]

-  }

   method Append(t)

-  {

     Contents := Contents + [t]

-  }

 }

 model ExtensibleArray[T] {

   var elements: array[T]

diff --git a/Test/jennisys0/ExtensibleArray.jen b/Test/jennisys0/ExtensibleArray.jen
index b7227d25..e6141ab7 100644
--- a/Test/jennisys0/ExtensibleArray.jen
+++ b/Test/jennisys0/ExtensibleArray.jen
@@ -2,26 +2,18 @@ class ExtensibleArray[T] {
   var Contents: seq[T]

 

   constructor Init()

-  {

     Contents := []

-  }

 

   method Get(i) returns (t)

     requires 0 <= i && i < |Contents|

-  {

     t := Contents[i]

-  }

 

   method Set(i, t)

     requires 0 <= i && i < |Contents|

-  {

     Contents := Contents[i := t]

-  }

 

   method Append(t)

-  {

     Contents := Contents + [t]

-  }

 }

 

 model ExtensibleArray[T] {

diff --git a/Test/jennisys0/Prog0.jen b/Test/jennisys0/Prog0.jen
index cd847846..14f96628 100644
--- a/Test/jennisys0/Prog0.jen
+++ b/Test/jennisys0/Prog0.jen
@@ -2,31 +2,28 @@ class C {
   var a: seq[int]

   var x: int

   constructor Init()

-  { }

   method Update(d)

-  {

     x := x + 1

     { nested := statement yes := sirrie }

     x.f := (12 + true)[8000 := 0 <= n]

-  }

   method Query() returns (r)

     requires r

     requires true

-    requires *

+    requires a[*]

     requires r.r.s

     requires a[i]

     requires a[i := 58]

     requires (((hello)))

     requires (((hello) + (goodbye)) - soonyousoon)

     requires 0 <= r

-  { }

+    { }

   method ManyParams(x:bool,y) returns (r,s:set[MyClass],t)

-  { }

 }

 

 model C {

   var x: int

-  frame xyz

+  frame xyz * abc * klm

+     mno pqr

   invariant x <= x

 }