assigning_meanings_to_programs.mlw 1.09 KB
Newer Older
1 2 3 4 5 6
(* Program proofs from Floyd's "Assigning Meanings to Programs" (1967) *)

module Sum

  (* computes the sum a[1] + ... + a[n] *)

7 8 9 10
  use int.Int
  use ref.Ref
  use array.Array
  use array.ArraySum
11 12 13 14 15

  let sum (a: array int) (n: int)
    requires { 0 <= n < a.length }
    ensures  { result = sum a 1 (n+1) }
  = let i = ref 1 in
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
    let s = ref 0 in
    while !i <= n do
      invariant { 1 <= !i <= n+1 /\ !s = sum a 1 !i }
      variant { n - !i }
      s := !s + a[!i];
      i := !i + 1
    done;
    !s

end

module Division

  (* Quotient and remainder of X div Y

     Floyd's lexicographic variant is unnecessarily complex here, since
     we do not seek for a variant which decreases at each statement, but
     only at each execution of the loop body. *)

35 36
  use int.Int
  use ref.Ref
37

38
  let division (x: int) (y: int) : (q: int, r: int)
39
    requires { 0 <= x /\ 0 < y }
40
    ensures  { 0 <= r < y /\ x = q * y + r }
41
  = let q = ref 0 in
42 43 44 45 46 47 48
    let r = ref x in
    while !r >= y do
      invariant { 0 <= !r /\ x = !q * y + !r }
      variant { !r }
      r := !r - y;
      q := !q + 1
    done;
49
    !q, !r
50 51

end