new example: binary multiplication

parent 4813b033
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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" memlimit="1000"/>
<file name="../binary_multiplication.mlw" expanded="true">
<theory name="BinaryMultiplication" sum="4446a95f7ced5daf85b69dec1d36a0fd" 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>
</goal>
</theory>
</file>
</why3session>
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