binary_multiplication: new-system-compliant code and a few comments

parent c7fda0d5
(* 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 import mach.int.Int
use import number.Parity
use import ref.Ref
let binary_mult (a b: int)
......@@ -15,7 +23,7 @@ module BinaryMultiplication
invariant { 0 <= !y }
invariant { !z + !x * !y = a * b }
variant { !y }
if odd !y then z := !z + !x;
if !y % 2 = 1 then z := !z + !x;
x := 2 * !x;
y := !y / 2
done;
......
......@@ -4,9 +4,9 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" expanded="true">
<theory name="BinaryMultiplication" sum="9c13d5392381b04161f82c19fb28f95e" expanded="true">
<theory name="BinaryMultiplication" sum="94846d4b1de94154d88628a5fe380629" expanded="true">
<goal name="WP_parameter binary_mult" expl="VC for binary_mult" expanded="true">
<proof prover="0"><result status="valid" time="0.74" steps="88"/></proof>
<proof prover="0"><result status="valid" time="0.74" steps="47"/></proof>
</goal>
</theory>
</file>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment