diff options
Diffstat (limited to 'Test/textbook/TuringFactorial.bpl')
-rw-r--r-- | Test/textbook/TuringFactorial.bpl | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl index dffc36ab..de00e3c0 100644 --- a/Test/textbook/TuringFactorial.bpl +++ b/Test/textbook/TuringFactorial.bpl @@ -1,35 +1,35 @@ -// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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));
+// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// 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)); |