examples/binary_multiplication.mlw

   1
   2 (** {1 Russian peasant multiplication}
   3
   4    Multiply two integers a and b using only addition, multiplication by 2,
   5    and division by 2.
   6
   7    Note: this is exactly the same algorithm as exponentiation by squaring
   8    with power/*/1 being replaced by */+/0.
   9 *)
  10
  11 module BinaryMultiplication
  12
  13   use mach.int.Int
  14   use ref.Ref
  15
  16   let binary_mult (a b: int) : int
  17     requires { b >= 0 }
  18     ensures  { result = a * b }
  19   = let x = ref a in
  20     let y = ref b in
  21     let z = ref 0 in
  22     while !y <> 0 do
  23       invariant { 0 <= !y }
  24       invariant { !z + !x * !y = a * b }
  25       variant   { !y }
  26       if !y % 2 = 1 then z := !z + !x;
  27       x := 2 * !x;
  28       y := !y / 2
  29     done;
  30     !z
  31
  32 end
  33
  34 (** Now using machine integers.
  35
  36     Assuming that the product fits in machine integers, we can still
  37     verify the code. The only exception is when `a*b = min_int`.
  38
  39     The code below makes no assumption on the sign of `b`.
  40     Instead, it uses the fact that `!y % 2` has the sign of `!y`
  41     so that `!x` is either added to or subtracted from the result.
  42 *)
  43
  44 module BinaryMultiplication63
  45
  46   use int.Int
  47   use int.Abs
  48   use mach.int.Int63
  49   use ref.Ref
  50
  51   let binary_mult (a b: int63) : int63
  52     requires { min_int < a * b <= max_int }
  53     ensures  { result = a * b }
  54   = let x = ref a in
  55     let y = ref b in
  56     let z = ref 0 in
  57     while !y <> 0 do
  58       invariant { if a*b >= 0 then !x * !y >= 0 && !z >= 0
  59                               else !x * !y <= 0 && !z <= 0 }
  60       invariant { !z + !x * !y = a * b }
  61       variant   { abs !y }
  62       z := !z + !x * (!y % 2);
  63       y := !y / 2;
  64       (* be careful not to make the very last multiplication *)
  65       if !y <> 0 then x := 2 * !x
  66     done;
  67     !z
  68
  69 end