examples/assigning_meanings_to_programs.mlw

   1 (* Program proofs from Floyd's "Assigning Meanings to Programs" (1967) *)
   2
   3 module Sum
   4
   5   (* computes the sum a[1] + ... + a[n] *)
   6
   7   use int.Int
   8   use ref.Ref
   9   use array.Array
  10   use array.ArraySum
  11
  12   let sum (a: array int) (n: int) : int
  13     requires { 0 <= n < a.length }
  14     ensures  { result = sum a 1 (n+1) }
  15   = let ref i = 1 in
  16     let ref s = 0 in
  17     while i <= n do
  18       invariant { 1 <= i <= n+1 /\ s = sum a 1 i }
  19       variant   { n - i }
  20       s <- s + a[i];
  21       i <- i + 1
  22     done;
  23     s
  24
  25 end
  26
  27 module Division
  28
  29   (* Quotient and remainder of X div Y
  30
  31      Floyd's lexicographic variant is unnecessarily complex here, since
  32      we do not seek for a variant which decreases at each statement, but
  33      only at each execution of the loop body. *)
  34
  35   use int.Int
  36   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 ref q = 0 in
  42     let ref r = x in
  43     while r >= y do
  44       invariant { 0 <= r /\ x = q * y + r }
  45       variant   { r }
  46       r <- r - y;
  47       q <- q + 1
  48     done;
  49     q, r
  50
  51 end