Wiki Agenda Contact Version française

Binary multiplication

See this description on Wikipedia


Authors: Jean-Christophe Filliâtre

Topics: Arithmetic

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(* Ancient Egyptian Multiplication

   Multiply two integers a and b using only addition, multiplication by 2,
   and division by 2.

   Note: this is exactly the same algorithm as exponentiation by squaring
   with power/*/1 being replaced by */+/0.
*)

module BinaryMultiplication

  use mach.int.Int
  use 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 !y % 2 = 1 then z := !z + !x;
      x := 2 * !x;
      y := !y / 2
    done;
    !z

end

download ZIP archive

Why3 Proof Results for Project "binary_multiplication"

Theory "binary_multiplication.BinaryMultiplication": fully verified

ObligationsAlt-Ergo 1.30
VC binary_mult0.05