(* 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 import int.Int
  use import ref.Ref

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

  let main () =
    division 1000 42

end