diff options
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
|