(* Euclidean division

   1. Prove soundness, i.e. (division a b) returns an integer q such that
      a = bq+r and 0 <= r < b for some r.
      (You have to strengthen the precondition.)

      Do you have to require b <> 0? Why?

   2. Prove termination.
      (You may have to strengthen the precondition even further.)
*)

module Division

  use int.Int

  let division (a b: int) : int
    requires { a > 0 /\ b > 0 }
    ensures  { exists r: int. a = b * result + r /\ 0 <= r < b }
  =
    let ref q = 0 in
    let ref r = a in
    while r >= b do
      invariant { a = b * q + r /\ r >= 0 }
      variant { r }
      q <- q + 1;
      r <- r - b
    done;
    q

  let main () =
    division 1000 42

end