diff options
author | 2011-11-03 18:14:16 -0700 | |
---|---|---|
committer | 2011-11-03 18:14:16 -0700 | |
commit | c49bb84bde29ece7af3c469f1bf68298d2525ef4 (patch) | |
tree | e526ec2a9c0548931899bf1b450310dd5c4f6772 | |
parent | 6c60f50ada38466a462c3b272fc3a7a0c9d24557 (diff) |
Added some Dafny and Boogie test cases, including Turing's factorial program, Hoare's classic FIND, and some induction tests for negative integers
-rw-r--r-- | Test/dafny1/Answer | 20 | ||||
-rw-r--r-- | Test/dafny1/MoreInduction.dfy | 34 | ||||
-rw-r--r-- | Test/dafny2/Answer | 4 | ||||
-rw-r--r-- | Test/dafny2/Classics.dfy | 103 | ||||
-rw-r--r-- | Test/dafny2/runtest.bat | 4 | ||||
-rw-r--r-- | Test/textbook/Answer | 4 | ||||
-rw-r--r-- | Test/textbook/TuringFactorial.bpl | 33 | ||||
-rw-r--r-- | Test/textbook/runtest.bat | 3 |
8 files changed, 201 insertions, 4 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d53ae14b..ab10d944 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -88,8 +88,24 @@ Dafny program verifier finished with 33 verified, 0 errors Dafny program verifier finished with 141 verified, 0 errors
-------------------- MoreInduction.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
+MoreInduction.dfy(75,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(74,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MoreInduction.dfy(80,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(79,21): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MoreInduction.dfy(85,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(84,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MoreInduction.dfy(90,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(89,22): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 15 verified, 4 errors
-------------------- Celebrity.dfy --------------------
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index efba0963..84c32fb3 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -61,3 +61,37 @@ ghost method Lemma<X>(list: List<X>, ext: List<X>) }
}
}
+
+// ---------------------------------------------
+
+function NegFac(n: int): int
+ decreases -n;
+{
+ if -1 <= n then -1 else - NegFac(n+1) * n
+}
+
+ghost method LemmaAll()
+ ensures forall n :: NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
+{
+}
+
+ghost method LemmaOne(n: int)
+ ensures NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
+{
+}
+
+ghost method LemmaAll_Neg()
+ ensures forall n :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+{
+}
+
+ghost method LemmaOne_Neg(n: int)
+ ensures NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+{
+}
+
+ghost method LemmaOneWithDecreases(n: int)
+ ensures NegFac(n) <= -1; // here, the programmer gives a good well-founded order, so this verifies
+ decreases -n;
+{
+}
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index cc2e8acb..eed3eaa0 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -1,4 +1,8 @@ +-------------------- Classics.dfy --------------------
+
+Dafny program verifier finished with 5 verified, 0 errors
+
-------------------- SnapshotableTrees.dfy --------------------
Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/dafny2/Classics.dfy b/Test/dafny2/Classics.dfy new file mode 100644 index 00000000..68d9bf79 --- /dev/null +++ b/Test/dafny2/Classics.dfy @@ -0,0 +1,103 @@ +// A version of Turing's additive factorial program [Dr. A. Turing, "Checking a large routine",
+// In "Report of a Conference of High Speed Automatic Calculating Machines", pp. 67-69, 1949].
+
+function Factorial(n: nat): nat
+{
+ if n == 0 then 1 else n * Factorial(n-1)
+}
+
+method AdditiveFactorial(n: nat) returns (u: nat)
+ ensures u == Factorial(n);
+{
+ u := 1;
+ var r := 0;
+ while (r < n)
+ invariant 0 <= r <= n;
+ invariant u == Factorial(r);
+ {
+ var v := u;
+ var s := 1;
+ while (s <= r)
+ invariant 1 <= s <= r+1;
+ invariant u == s * Factorial(r);
+ {
+ u := u + v;
+ s := s + 1;
+ }
+ r := r + 1;
+ }
+}
+
+// Hoare's FIND program [C.A.R. Hoare, "Proof of a program: FIND", CACM 14(1): 39-45, 1971].
+// The proof annotations here are not the same as in Hoare's article.
+
+// In Hoare's words:
+// This program operates on an array A[1:N], and a value of f (1 <= f <= N).
+// Its effect is to rearrange the elements of A in such a way that:
+// forall p,q (1 <= p <= f <= q <= N ==> A[p] <= A[f] <= A[q]).
+//
+// Here, we use 0-based indices, so we would say:
+// This method operates on an array A[0..N], and a value of f (0 <= f < N).
+// Its effect is to rearrange the elements of A in such a way that:
+// forall p,q :: 0 <= p <= f <= q < N ==> A[p] <= A[f] <= A[q]).
+
+method FIND(A: array<int>, N: int, f: int)
+ requires A != null && A.Length == N;
+ requires 0 <= f < N;
+ modifies A;
+ ensures forall p,q :: 0 <= p <= f <= q < N ==> A[p] <= A[q];
+{
+ var m, n := 0, N-1;
+ while (m < n)
+ invariant 0 <= m <= f <= n < N;
+ invariant forall p,q :: 0 <= p < m <= q < N ==> A[p] <= A[q];
+ invariant forall p,q :: 0 <= p <= n < q < N ==> A[p] <= A[q];
+ {
+ var r, i, j := A[f], m, n;
+ while (i <= j)
+ invariant m <= i && j <= n;
+ invariant -1 <= j && i <= N;
+ invariant i <= j ==> exists g :: i <= g < N && r <= A[g];
+ invariant i <= j ==> exists g :: 0 <= g <= j && A[g] <= r;
+ invariant forall p :: 0 <= p < i ==> A[p] <= r;
+ invariant forall q :: j < q < N ==> r <= A[q];
+ // the following two invariants capture (and follow from) the fact that the array is not modified outside the [m:n] range
+ invariant forall p,q :: 0 <= p < m <= q < N ==> A[p] <= A[q];
+ invariant forall p,q :: 0 <= p <= n < q < N ==> A[p] <= A[q];
+ // the following invariant is used to prove progress of the outer loop
+ invariant (i==m && j==n && r==A[f]) || (m<i && j<n);
+ {
+ ghost var firstIteration := i==m && j==n;
+ while (A[i] < r)
+ invariant m <= i <= N && (firstIteration ==> i <= f);
+ invariant exists g :: i <= g < N && r <= A[g];
+ invariant exists g :: 0 <= g <= j && A[g] <= r;
+ invariant forall p :: 0 <= p < i ==> A[p] <= r;
+ decreases j - i;
+ { i := i + 1; }
+
+ while (r < A[j])
+ invariant 0 <= j <= n && (firstIteration ==> f <= j);
+ invariant exists g :: i <= g < N && r <= A[g];
+ invariant exists g :: 0 <= g <= j && A[g] <= r;
+ invariant forall q :: j < q < N ==> r <= A[q];
+ decreases j;
+ { j := j - 1; }
+
+ assert A[j] <= r <= A[i];
+ if (i <= j) {
+ var w := A[i]; A[i] := A[j]; A[j] := w; // swap A[i] and A[j] (which may be referring to the same location)
+ assert A[i] <= r <= A[j];
+ i, j := i + 1, j - 1;
+ }
+ }
+
+ if (f <= j) {
+ n := j;
+ } else if (i <= f) {
+ m := i;
+ } else {
+ break; // Hoare used a goto
+ }
+ }
+}
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index f6f25429..50b4ca18 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -5,7 +5,9 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
-for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy
+for %%f in (
+ Classics.dfy
+ SnapshotableTrees.dfy TreeBarrier.dfy
COST-verif-comp-2011-1-MaxArray.dfy
COST-verif-comp-2011-2-MaxTree-class.dfy
COST-verif-comp-2011-2-MaxTree-datatype.dfy
diff --git a/Test/textbook/Answer b/Test/textbook/Answer index 50e96aca..dace3eb3 100644 --- a/Test/textbook/Answer +++ b/Test/textbook/Answer @@ -18,3 +18,7 @@ Boogie program verifier finished with 2 verified, 0 errors ------------------------------ McCarthy-91.bpl ---------------------
Boogie program verifier finished with 1 verified, 0 errors
+
+------------------------------ TuringFactorial.bpl ---------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl new file mode 100644 index 00000000..37a3cb46 --- /dev/null +++ b/Test/textbook/TuringFactorial.bpl @@ -0,0 +1,33 @@ +// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
+// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
+// pp. 67-69, 1949.
+
+procedure ComputeFactorial(n: int) returns (u: int)
+ requires 1 <= n;
+ ensures u == Factorial(n);
+{
+ var r, v, s: int;
+ r, u := 1, 1;
+TOP: // B
+ assert r <= n;
+ assert u == Factorial(r);
+ v := u;
+ if (n <= r) { return; }
+ s := 1;
+INNER: // E
+ assert s <= r;
+ assert v == Factorial(r) && u == s * Factorial(r);
+ u := u + v;
+ s := s + 1;
+ assert s - 1 <= r;
+ if (s <= r) { goto INNER; }
+ r := r + 1;
+ goto TOP;
+}
+
+function Factorial(int): int;
+axiom Factorial(0) == 1;
+axiom (forall n: int :: {Factorial(n)} 1 <= n ==> Factorial(n) == n * Factorial_Aux(n-1));
+
+function Factorial_Aux(int): int;
+axiom (forall n: int :: {Factorial(n)} Factorial(n) == Factorial_Aux(n));
diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat index 265aa071..b747312d 100644 --- a/Test/textbook/runtest.bat +++ b/Test/textbook/runtest.bat @@ -6,7 +6,8 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe REM ======================
REM ====================== Examples written in Boogie
REM ======================
-for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl) do (
+for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl
+ TuringFactorial.bpl) do (
echo.
echo ------------------------------ %%f ---------------------
%BPLEXE% %* %%f
|