Commit b8c5222c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: binary_multiplication with 63-bit integers

parent cbfb1d83
(* Ancient Egyptian Multiplication
(** {1 Russian peasant multiplication}
Multiply two integers a and b using only addition, multiplication by 2,
and division by 2.
......@@ -13,7 +13,7 @@ module BinaryMultiplication
use mach.int.Int
use ref.Ref
let binary_mult (a b: int)
let binary_mult (a b: int) : int
requires { b >= 0 }
ensures { result = a * b }
= let x = ref a in
......@@ -30,3 +30,40 @@ module BinaryMultiplication
!z
end
(** Now using machine integers.
Assuming that the product fits in machine integers, we can still
verify the code. The only exception is when `a*b = min_int`.
The code below makes no assumption on the sign of `b`.
Instead, it uses the fact that `!y % 2` has the sign of `!y`
so that `!x` is either added to or subtracted from the result.
*)
module BinaryMultiplication63
use int.Int
use int.Abs
use mach.int.Int63
use ref.Ref
let binary_mult (a b: int63) : int63
requires { min_int < a * b <= max_int }
ensures { result = a * b }
= let x = ref a in
let y = ref b in
let z = ref 0 in
while !y <> 0 do
invariant { if a*b >= 0 then !x * !y >= 0 && !z >= 0
else !x * !y <= 0 && !z <= 0 }
invariant { !z + !x * !y = a * b }
variant { abs !y }
z := !z + !x * (!y % 2);
y := !y / 2;
(* be careful not to make the very last multiplication *)
if !y <> 0 then x := 2 * !x
done;
!z
end
......@@ -3,11 +3,66 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_multiplication.mlw" proved="true">
<theory name="BinaryMultiplication" proved="true">
<goal name="VC binary_mult" expl="VC for binary_mult" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="63"/></proof>
</goal>
</theory>
<theory name="BinaryMultiplication63" proved="true">
<goal name="VC binary_mult" expl="VC for binary_mult" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC binary_mult.0" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_mult.1" expl="loop invariant init" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_mult.2" expl="division by zero" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_mult.3" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_mult.4" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC binary_mult.5" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC binary_mult.6" expl="division by zero" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC binary_mult.7" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_mult.8" expl="integer overflow" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC binary_mult.9" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_mult.10" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC binary_mult.11" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.73"/></proof>
</goal>
<goal name="VC binary_mult.12" expl="loop variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC binary_mult.13" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC binary_mult.14" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC binary_mult.15" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</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