Toccata

(* Program proofs from Floyd's "Assigning Meanings to Programs" (1967) *)

module Sum

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

  use int.Int
  use ref.Ref
  use array.Array
  use array.ArraySum

  let sum (a: array int) (n: int) : int
    requires { 0 <= n < a.length }
    ensures  { result = sum a 1 (n+1) }
  = let ref i = 1 in
    let ref s = 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. *)

  use int.Int
  use ref.Ref

  let division (x: int) (y: int) : (q: int, r: int)
    requires { 0 <= x /\ 0 < y }
    ensures  { 0 <= r < y /\ x = q * y + r }
  = let ref q = 0 in
    let ref r = x in
    while r >= y do
      invariant { 0 <= r /\ x = q * y + r }
      variant   { r }
      r <- r - y;
      q <- q + 1
    done;
    q, r

end