why3/examples/checking_a_large_routine.mlw

(* '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