examples/checking_a_large_routine.mlw

   1 (* 'Checking a large routine' Alan Mathison Turing, 1949
   2
   3    One of the earliest proof of program.
   4    The routine computes n! using only additions, with two nested loops.
   5 *)
   6
   7 module CheckingALargeRoutine
   8
   9   use int.Int
  10   use int.Fact
  11   use ref.Ref
  12
  13   (* using 'while' loops, to keep close to Turing's flowchart *)
  14   let routine (n: int) requires { n >= 0 } ensures { result = fact n } =
  15     let r = ref 0 in
  16     let u = ref 1 in
  17     while !r < n do
  18       invariant { 0 <= !r <= n /\ !u = fact !r }
  19       variant   { n - !r }
  20       let s = ref 1 in
  21       let v = !u in
  22       while !s <= !r do
  23         invariant { 1 <= !s <= !r + 1 /\ !u = !s * fact !r }
  24         variant   { !r - !s }
  25         u := !u + v;
  26         s := !s + 1
  27       done;
  28       r := !r + 1
  29     done;
  30     !u
  31
  32   (* using 'for' loops, for clearer code and annotations *)
  33   let routine2 (n: int) requires { n >= 0 } ensures { result = fact n } =
  34     let u = ref 1 in
  35     for r = 0 to n-1 do invariant { !u = fact r }
  36       let v = !u in
  37       for s = 1 to r do invariant { !u = s * fact r }
  38         u := !u + v
  39       done
  40     done;
  41     !u
  42
  43   let downward (n: int) requires { n >= 0 } ensures { result = fact n } =
  44     let r = ref n in
  45     let u = ref 1 in
  46     while !r <> 0 do
  47       invariant { 0 <= !r <= n /\ !u * fact !r = fact n }
  48       variant   { !r }
  49       let s = ref 1 in
  50       let v = !u in
  51       while !s <> !r do
  52         invariant { 1 <= !s <= !r /\ !u = !s * v }
  53         variant   { !r - !s }
  54         u := !u + v;
  55         s := !s + 1
  56       done;
  57       r := !r - 1
  58     done;
  59     !u
  60
  61 end