From e530ac46773698484d3b8881d5b1d4a3742b37d7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 26 Jul 2011 13:29:17 -0700 Subject: 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) --- Test/VSI-Benchmarks/Answer | 12 ++++++++++++ Test/VSI-Benchmarks/runtest.bat | 4 +--- Test/dafny1/Answer | 6 +++--- Test/dafny1/Celebrity.dfy | 26 +++++++------------------- Test/dafny1/Rippling.dfy | 18 ++++++++---------- Test/dafny1/UltraFilter.dfy | 3 --- 6 files changed, 31 insertions(+), 38 deletions(-) (limited to 'Test') 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; - -function method Knows(a: Person, b: Person): bool - reads this; +static function method Knows(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): bool - reads this; + +static function IsCelebrity(c: Person, people: set): bool { c in people && (forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p)) } -method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) +method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) requires (exists c :: IsCelebrity(c, people)); ensures r == c; { @@ -28,7 +17,7 @@ method FindCelebrity0(people: set, ghost c: Person) returns (r: Person) r := cc; } -method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) +method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) requires IsCelebrity(c, people); ensures r == c; { @@ -51,7 +40,7 @@ method FindCelebrity1(people: set, ghost c: Person) returns (r: Person) r := x; } -method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) +method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) requires IsCelebrity(c, people); ensures r == c; { @@ -75,7 +64,7 @@ method FindCelebrity2(people: set, ghost c: Person) returns (r: Person) } r := b; } -/* + method FindCelebrity3(n: int, people: set, 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, 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 { // Dafny currently does not have a set comprehension expression, so this method stub will have to do method H(f: set>, S: set, M: set) returns (h: set>) ensures (forall X :: X in h <==> M + X in f); - { - assume false; - } method Lemma_HIsFilter(h: set>, f: set>, S: set, M: set) requires IsFilter(f, S); -- cgit v1.2.3