Dafny: re-ran parser generator to include semicolon-less body-less functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)

6 files changed, 31 insertions, 38 deletions

diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer
index e2456408..2a4587f4 100644
--- a/Test/VSI-Benchmarks/Answer
+++ b/Test/VSI-Benchmarks/Answer
@@ -7,6 +7,10 @@ Dafny program verifier finished with 10 verified, 0 errors
 

 Dafny program verifier finished with 6 verified, 0 errors

 

+-------------------- b3.dfy --------------------

+

+Dafny program verifier finished with 10 verified, 0 errors

+

 -------------------- b4.dfy --------------------

 

 Dafny program verifier finished with 11 verified, 0 errors

@@ -18,3 +22,11 @@ Dafny program verifier finished with 22 verified, 0 errors
 -------------------- b6.dfy --------------------

 

 Dafny program verifier finished with 21 verified, 0 errors

+

+-------------------- b7.dfy --------------------

+

+Dafny program verifier finished with 23 verified, 0 errors

+

+-------------------- b8.dfy --------------------

+

+Dafny program verifier finished with 42 verified, 0 errors

diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat
index 799e1d40..a733a1c0 100644
--- a/Test/VSI-Benchmarks/runtest.bat
+++ b/Test/VSI-Benchmarks/runtest.bat
@@ -6,9 +6,7 @@ set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
 set BPLEXE=%BOOGIEDIR%\Boogie.exe

 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

-REM b3, b7 and b8 need reworking to not use body-less functions and methods.

-

-for %%f in (b1.dfy b2.dfy b4.dfy b5.dfy b6.dfy) do (

+for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (

   echo.

   echo -------------------- %%f --------------------

 

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 5bb746d8..5ee9f921 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -85,12 +85,12 @@ Dafny program verifier finished with 29 verified, 0 errors
 

 -------------------- Rippling.dfy --------------------

 

-Dafny program verifier finished with 122 verified, 0 errors

+Dafny program verifier finished with 132 verified, 0 errors

 

 -------------------- Celebrity.dfy --------------------

 

-Dafny program verifier finished with 8 verified, 0 errors

+Dafny program verifier finished with 10 verified, 0 errors

 

 -------------------- UltraFilter.dfy --------------------

 

-Dafny program verifier finished with 20 verified, 0 errors

+Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index a10c4324..21b895aa 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,26 +1,15 @@
 // Celebrity example, inspired by the Rodin tutorial

 

-class Person

-{

-

-}

-

-var pa: seq<Person>;

-

-function method Knows(a: Person, b: Person): bool

-  reads this;

+static function method Knows<Person>(a: Person, b: Person): bool

   requires a != b;  // forbid asking about the reflexive case

-{

-   exists i | 0 <= i && i < |pa| :: 0 <= i < |pa| / 2 ==> pa[2*i] == a && pa[2*i+1] == b

-}

-function IsCelebrity(c: Person, people: set<Person>): bool

-  reads this;

+

+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool

 {

   c in people &&

   (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))

 }

 

-method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)

+method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

   requires (exists c :: IsCelebrity(c, people));

   ensures r == c;

 {

@@ -28,7 +17,7 @@ method FindCelebrity0(people: set<Person>, ghost c: Person) returns (r: Person)
   r := cc;

 }

 

-method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)

+method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

   requires IsCelebrity(c, people);

   ensures r == c;

 {

@@ -51,7 +40,7 @@ method FindCelebrity1(people: set<Person>, ghost c: Person) returns (r: Person)
   r := x;

 }

 

-method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)

+method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)

   requires IsCelebrity(c, people);

   ensures r == c;

 {

@@ -75,7 +64,7 @@ method FindCelebrity2(people: set<Person>, ghost c: Person) returns (r: Person)
   }

   r := b;

 }

-/*

+

 method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)

   requires 0 < n;

   requires (forall p :: p in people <==> 0 <= p && p < n);

@@ -99,4 +88,3 @@ method FindCelebrity3(n: int, people: set<int>, ghost c: int) returns (r: int)
   }

   r := b;

 }

-*/
\ No newline at end of file
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 78905b6e..0a4d541d 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -157,14 +157,13 @@ function last(xs: List): Nat
     case Cons(z, zs) => last(ys)

 }

 

-/*

 function mapF(xs: List): List

 {

   match xs

   case Nil => Nil

   case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))

 }

-function HardcodedUninterpretedFunction(n: Nat): Nat*/

+function HardcodedUninterpretedFunction(n: Nat): Nat

 

 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

@@ -187,7 +186,7 @@ function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List
     else Cons(y, ys)

 }

 

-/*function filterP(xs: List): List

+function filterP(xs: List): List

 {

   match xs

   case Nil => Nil

@@ -196,7 +195,7 @@ function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List
     then Cons(y, filterP(ys))

     else filterP(ys)

 }

-function HardcodedUninterpretedPredicate(n: Nat): Bool*/

+function HardcodedUninterpretedPredicate(n: Nat): Bool

 

 function insort(n: Nat, xs: List): List

 {

@@ -328,22 +327,21 @@ ghost method P11()
 {

 }

 

-/*

 ghost method P12()

   ensures (forall n, xs :: drop(n, mapF(xs)) == mapF(drop(n, xs)));

 {

-}*/

+}

 

 ghost method P13()

   ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));

 {

 }

-/*

+

 ghost method P14()

   ensures (forall xs, ys :: filterP(concat(xs, ys)) == concat(filterP(xs), filterP(ys)));

 {

 }

-*/

+

 ghost method P15()

   ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));

 {

@@ -480,12 +478,12 @@ ghost method P40()
   ensures (forall xs :: take(Zero, xs) == Nil);

 {

 }

-/*

+

 ghost method P41()

   ensures (forall n, xs :: take(n, mapF(xs)) == mapF(take(n, xs)));

 {

 }

-*/

+

 ghost method P42()

   ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));

 {

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 0dfb6683..c8419890 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -31,9 +31,6 @@ class UltraFilter<G> {
   // Dafny currently does not have a set comprehension expression, so this method stub will have to do

   method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)

     ensures (forall X :: X in h <==> M + X in f);

-  {

-    assume false;

-  }

 

   method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)

     requires IsFilter(f, S);