(* Russian multiplication
Multiply two integers a and b using only addition, multiplication by 2,
and division by 2. You may assume b to be nonnegative.
Note: library int.ComputerDivision (already imported) provide functions
"div" and "mod".
Questions:
1. Prove soundness of function multiplication.
2. Prove its termination
i.e. remove "diverges" and add a "variant" to the loop.
*)
use int.Int
use int.ComputerDivision
use ref.Ref
let multiplication (a b: int) : int
requires { true }
diverges
ensures { true }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { true }
if mod !y 2 = 1 then z := !z + !x;
x := 2 * !x;
y := div !y 2
done;
!z
(* Note: this is exactly the same algorithm as exponentiation by squarring
with power/*/1 being replaced by */+/0.
*)