(* 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