## 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

Obligations | Alt-Ergo 1.30 |

VC binary_mult | 0.05 |