Added some Dafny and Boogie test cases, including Turing's factorial program, Hoare's classic FIND, and some induction tests for negative integers

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