diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-03 18:14:16 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-03 18:14:16 -0700 |
| commit | c49bb84bde29ece7af3c469f1bf68298d2525ef4 (patch) | |
| tree | e526ec2a9c0548931899bf1b450310dd5c4f6772 /Test/textbook | |
| 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
Diffstat (limited to 'Test/textbook')
| -rw-r--r-- | Test/textbook/Answer | 4 | ||||
| -rw-r--r-- | Test/textbook/TuringFactorial.bpl | 33 | ||||
| -rw-r--r-- | Test/textbook/runtest.bat | 3 |
3 files changed, 39 insertions, 1 deletions
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
|