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

  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 q = ref 0 in
    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;
    !q, !r

end