From c49bb84bde29ece7af3c469f1bf68298d2525ef4 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 3 Nov 2011 18:14:16 -0700
Subject: Added some Dafny and Boogie test cases, including Turing's factorial
 program, Hoare's classic FIND, and some induction tests for negative integers

---
 Test/textbook/Answer              |  4 ++++
 Test/textbook/TuringFactorial.bpl | 33 +++++++++++++++++++++++++++++++++
 Test/textbook/runtest.bat         |  3 ++-
 3 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 Test/textbook/TuringFactorial.bpl

(limited to 'Test/textbook')

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
-- 
cgit v1.2.3