binary_multiplication.mlw 461 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25

module BinaryMultiplication

  use import mach.int.Int
  use import number.Parity
  use import ref.Ref

  let binary_mult (a b: int)
    requires { b >= 0 }
    ensures  { result = a * b }
  = let x = ref a in
    let y = ref b in
    let z = ref 0 in
    while !y <> 0 do
      invariant { 0 <= !y }
      invariant { !z + !x * !y = a * b }
      variant   { !y }
      if odd !y then z := !z + !x;
      x := 2 * !x;
      y := !y / 2
    done;
    !z

end