Skip to content

why3
why3
Commit f9ed8bcc authored by Martin Clochard's avatar Martin Clochard
Browse files
Options

verifythis_2016_matrix_multiplication: change exists to even

parent 16684355
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 473 additions and 478 deletions
examples/verifythis_2016_matrix_multiplication/naive.mlw
View file @ f9ed8bcc
......@@ -16,7 +16,7 @@ module MatrixMultiplication
ensures { result.rows = a.rows /\ result.columns = b.columns }
ensures { matrix_product result a b }
= let rs = make (rows a) (columns b) 0 in
for i = 0 to rows a - 1 do
for i = 0 to a.rows - 1 do
invariant { forall i0 j0. i <= i0 < rows a /\ 0 <= j0 < columns b ->
rs.elts[i0][j0] = 0 }
invariant { forall i0 j0. 0 <= i0 < i /\ 0 <= j0 < columns b ->
......
examples/verifythis_2016_matrix_multiplication/naive/why3session.xml
View file @ f9ed8bcc
......@@ -2,85 +2,85 @@
<!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="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../naive.mlw">
<theory name="MatrixMultiplication" sum="888d777f6b0bead427ee1083245abb55">
<goal name="WP_parameter mult_naive" expl="VC for mult_naive">
<transf name="split_goal_wp">
<goal name="WP_parameter mult_naive.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter mult_naive.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter mult_naive.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter mult_naive.4" expl="4. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter mult_naive.5" expl="5. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter mult_naive.6" expl="6. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter mult_naive.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter mult_naive.8" expl="8. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter mult_naive.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter mult_naive.10" expl="10. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter mult_naive.11" expl="11. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter mult_naive.12" expl="12. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter mult_naive.13" expl="13. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="WP_parameter mult_naive.14" expl="14. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter mult_naive.15" expl="15. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter mult_naive.16" expl="16. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter mult_naive.17" expl="17. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="38"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="41"/></proof>
</goal>
<goal name="WP_parameter mult_naive.18" expl="18. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.19" steps="73"/></proof>
<proof prover="1"><result status="valid" time="0.06" steps="56"/></proof>
</goal>
<goal name="WP_parameter mult_naive.19" expl="19. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter mult_naive.20" expl="20. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="WP_parameter mult_naive.21" expl="21. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter mult_naive.22" expl="22. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="46"/></proof>
<proof prover="1"><result status="valid" time="0.03" steps="40"/></proof>
</goal>
<goal name="WP_parameter mult_naive.23" expl="23. type invariant">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter mult_naive.24" expl="24. postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter mult_naive.25" expl="25. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
</transf>
</goal>
......
examples/verifythis_2016_matrix_multiplication/strassen.mlw
View file @ f9ed8bcc
......@@ -264,23 +264,20 @@ module MatrixMultiplication
use import int.EuclideanDivision
use import number.Parity
let rec strassen (a b: matrix int) (ghost flag:int) : matrix int
requires { a.mdl.F.cols = b.mdl.F.rows }
requires { flag >= 0 }
requires { flag = 0 ->
a.mdl.F.rows = 1 \/ a.mdl.F.cols = 1 \/ b.mdl.F.cols = 1 \/
exists k l m. a.mdl.F.rows = 2*k
/\ a.mdl.F.cols = 2*l
/\ b.mdl.F.cols = 2*m }
(even a.mdl.F.rows /\ even a.mdl.F.cols /\ even b.mdl.F.cols) }
ensures { result.mdl = mul a.mdl b.mdl }
ensures { result.mdl.F.rows = a.mdl.F.rows }
ensures { result.mdl.F.cols = b.mdl.F.cols }
variant { a.mdl.F.rows + a.mdl.F.cols + b.mdl.F.cols + 3 * flag, flag }
= let cut_off = abstract ensures { result >= 1 } 42 end in
let rw = a.rows in
let md = a.columns in
let cl = b.columns in
let (rw, md, cl)= (a.rows, a.columns, b.columns) in
assert { rw = a.mdl.F.rows /\ md = a.mdl.F.cols /\ cl = b.mdl.F.cols };
if rw <= cut_off || md <= cut_off || cl <= cut_off
then mul_naive a b else
......@@ -288,14 +285,12 @@ module MatrixMultiplication
requires { 0 <= n }
returns { (q,r) -> n = 2 * q + r /\ 0 <= r <= 1 /\ n + r = 2 * (q+r) }
= (div n 2,mod n 2) in
let (qr,rr) = div2 rw in
let (qm,rm) = div2 md in
let (qc,rc) = div2 cl in
let (qr, rr) = div2 rw in
let (qm, rm) = div2 md in
let (qc, rc) = div2 cl in
if rr <> 0 || rm <> 0 || rc <> 0
then begin (* Padding *)
let rw' = rw + rr in
let md' = md + rm in
let cl' = cl + rc in
let (rw', md', cl') = (rw + rr, md + rm, cl + rc) in
let ap = padding a rw' md' in
let bp = padding b md' cl' in
let m = strassen ap bp 0 in
......
examples/verifythis_2016_matrix_multiplication/sum_extended/why3session.xml
View file @ f9ed8bcc
......@@ -2,46 +2,46 @@
<!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="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../sum_extended.mlw">
<theory name="Sum_extended" sum="cfab2f022b7b9478b4cc84f0f10fa2ed">
<goal name="WP_parameter sum_mult" expl="VC for sum_mult">
<proof prover="0"><result status="valid" time="0.05" steps="24"/></proof>
<proof prover="1"><result status="valid" time="0.05" steps="36"/></proof>
</goal>
<goal name="WP_parameter sum_add" expl="VC for sum_add">
<proof prover="0"><result status="valid" time="0.04" steps="37"/></proof>
<proof prover="1"><result status="valid" time="0.22" steps="260"/></proof>
</goal>
<goal name="WP_parameter fubini" expl="VC for fubini">
<transf name="split_goal_wp">
<goal name="WP_parameter fubini.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="WP_parameter fubini.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter fubini.3" expl="3. variant decrease">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="WP_parameter fubini.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter fubini.5" expl="5. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter fubini.5.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter fubini.5.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="27"/></proof>
<proof prover="1"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fubini.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter sum_ext" expl="VC for sum_ext">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="28"/></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