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
download ZIP archive