## Proof from Turing's Checking a Large Routine (1949)

A historical example: Checking A Large Routine by Alan Turing (1949) is one of the very first proof of program.

Authors: Jean-Christophe Filliâtre

Topics: Historical examples

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(* 'Checking a large routine' Alan Mathison Turing, 1949

One of the earliest proof of program.
The routine computes n! using only additions, with two nested loops.
*)

module CheckingALargeRoutine

use int.Int
use int.Fact
use ref.Ref

(* using 'while' loops, to keep close to Turing's flowchart *)
let routine (n: int) requires { n >= 0 } ensures { result = fact n } =
let r = ref 0 in
let u = ref 1 in
while !r < n do
invariant { 0 <= !r <= n /\ !u = fact !r }
variant   { n - !r }
let s = ref 1 in
let v = !u in
while !s <= !r do
invariant { 1 <= !s <= !r + 1 /\ !u = !s * fact !r }
variant   { !r - !s }
u := !u + v;
s := !s + 1
done;
r := !r + 1
done;
!u

(* using 'for' loops, for clearer code and annotations *)
let routine2 (n: int) requires { n >= 0 } ensures { result = fact n } =
let u = ref 1 in
for r = 0 to n-1 do invariant { !u = fact r }
let v = !u in
for s = 1 to r do invariant { !u = s * fact r }
u := !u + v
done
done;
!u

let downward (n: int) requires { n >= 0 } ensures { result = fact n } =
let r = ref n in
let u = ref 1 in
while !r <> 0 do
invariant { 0 <= !r <= n /\ !u * fact !r = fact n }
variant   { !r }
let s = ref 1 in
let v = !u in
while !s <> !r do
invariant { 1 <= !s <= !r /\ !u = !s * v }
variant   { !r - !s }
u := !u + v;
s := !s + 1
done;
r := !r - 1
done;
!u

end
```