(* Euclidean division
1. Prove soundness, i.e. (division a b) returns an integer q such that
a = bq+r and 0 <= r < b.
(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 { ... }
q := !q + 1;
r := !r - b
done;
!q
let test1 () =
let q = division 3 1 in
assert { q = 1 }
end