(* 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
i.e. remove "diverges" and add a "variant" to the loop.
(You may have to strengthen the precondition even further.)
*)
use int.Int
use ref.Ref
let division (a b: int) : int
requires { true }
diverges
ensures { exists r. 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 ()
diverges
=
division 1000 42