Commit 7f59fa34 authored by Martin Clochard's avatar Martin Clochard

update proof sessions

parent f181fd76
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
<file name="../matrices.mlw"> <file name="../matrices.mlw">
<theory name="MatrixGen" sum="d41d8cd98f00b204e9800998ecf8427e"> <theory name="MatrixGen" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory> </theory>
<theory name="Matrix" sum="862099dd531bba3a8ce8aca77f580ae7"> <theory name="Matrix" sum="ba7eca602ee03df2a98f7a686c251c65">
<goal name="set_def1"> <goal name="set_def1">
<proof prover="2"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
...@@ -21,17 +21,17 @@ ...@@ -21,17 +21,17 @@
<proof prover="2"><result status="valid" time="0.00" steps="22"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="22"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="FixedMatrix" sum="81d1f6ecddc981db1f906002ad2c6515"> <theory name="FixedMatrix" sum="5d486d0188577a056ee4b579fa3069c2">
<goal name="rows_and_cols_nonnegative"> <goal name="rows_and_cols_nonnegative">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="SquareFixedMatrix" sum="8866fe956f3cb17788b7229e8763a520"> <theory name="SquareFixedMatrix" sum="d58222172e1753dccc191aaf22a115ae">
<goal name="r_and_c_nonnegative"> <goal name="r_and_c_nonnegative">
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof> <proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal> </goal>
</theory> </theory>
<theory name="MatrixArithmetic" sum="179a17c543d2ee8c5d1128db6e7ac5b9"> <theory name="MatrixArithmetic" sum="51e672c189e950ed33557df63dcd9958">
<goal name="zero_neutral"> <goal name="zero_neutral">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="zero_neutral.1" expl="1."> <goal name="zero_neutral.1" expl="1.">
...@@ -78,25 +78,25 @@ ...@@ -78,25 +78,25 @@
<goal name="opposite_add"> <goal name="opposite_add">
<proof prover="0"><result status="valid" time="0.49"/></proof> <proof prover="0"><result status="valid" time="0.49"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_assoc_get" expl="VC for mul_assoc_get"> <goal name="VC mul_assoc_get" expl="VC for mul_assoc_get">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter mul_assoc_get.1" expl="1. precondition"> <goal name="VC mul_assoc_get.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.02" steps="22"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="22"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_assoc_get.2" expl="2. precondition"> <goal name="VC mul_assoc_get.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.04" steps="30"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="30"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_assoc_get.3" expl="3. assertion"> <goal name="VC mul_assoc_get.3" expl="3. assertion">
<proof prover="2"><result status="valid" time="0.06" steps="52"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="52"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_assoc_get.4" expl="4. precondition"> <goal name="VC mul_assoc_get.4" expl="4. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="35"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.05" steps="35"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_assoc_get.5" expl="5. assertion"> <goal name="VC mul_assoc_get.5" expl="5. assertion">
<proof prover="2"><result status="valid" time="0.04" steps="34"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="34"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_assoc_get.6" expl="6. postcondition"> <goal name="VC mul_assoc_get.6" expl="6. postcondition">
<proof prover="2"><result status="valid" time="0.02" steps="12"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -110,46 +110,46 @@ ...@@ -110,46 +110,46 @@
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter mul_distr_right_get" expl="VC for mul_distr_right_get"> <goal name="VC mul_distr_right_get" expl="VC for mul_distr_right_get">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter mul_distr_right_get.1" expl="1. assertion"> <goal name="VC mul_distr_right_get.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.06" steps="317"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.15" steps="274"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_distr_right_get.2" expl="2. precondition"> <goal name="VC mul_distr_right_get.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.10" steps="46"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.03" steps="46"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_distr_right_get.3" expl="3. postcondition"> <goal name="VC mul_distr_right_get.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.06" steps="112"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.13" steps="112"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="mul_distr_right"> <goal name="mul_distr_right">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="mul_distr_right.1" expl="1."> <goal name="mul_distr_right.1" expl="1.">
<proof prover="2"><result status="valid" time="0.05" steps="295"/></proof> <proof prover="2"><result status="valid" time="0.05" steps="297"/></proof>
</goal> </goal>
<goal name="mul_distr_right.2" expl="2."> <goal name="mul_distr_right.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="23"/></proof> <proof prover="2"><result status="valid" time="0.01" steps="23"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="WP_parameter mul_distr_left_get" expl="VC for mul_distr_left_get"> <goal name="VC mul_distr_left_get" expl="VC for mul_distr_left_get">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter mul_distr_left_get.1" expl="1. assertion"> <goal name="VC mul_distr_left_get.1" expl="1. assertion">
<proof prover="2"><result status="valid" time="0.19" steps="329"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.10" steps="286"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_distr_left_get.2" expl="2. precondition"> <goal name="VC mul_distr_left_get.2" expl="2. precondition">
<proof prover="2"><result status="valid" time="0.05" steps="46"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.04" steps="46"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_distr_left_get.3" expl="3. postcondition"> <goal name="VC mul_distr_left_get.3" expl="3. postcondition">
<proof prover="2"><result status="valid" time="0.05" steps="45"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.03" steps="45"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
<goal name="mul_distr_left"> <goal name="mul_distr_left">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="mul_distr_left.1" expl="1."> <goal name="mul_distr_left.1" expl="1.">
<proof prover="2"><result status="valid" time="0.04" steps="289"/></proof> <proof prover="2"><result status="valid" time="0.04" steps="288"/></proof>
</goal> </goal>
<goal name="mul_distr_left.2" expl="2."> <goal name="mul_distr_left.2" expl="2.">
<proof prover="2"><result status="valid" time="0.01" steps="23"/></proof> <proof prover="2"><result status="valid" time="0.01" steps="23"/></proof>
...@@ -179,20 +179,58 @@ ...@@ -179,20 +179,58 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="BlockMul" sum="a0d8b3f3a9391a77a23d88b4d4a63f23"> <theory name="BlockMul" sum="4b4a8b669c6aee7d1b50429c51fc5e29">
<goal name="WP_parameter block_mul_ij" expl="VC for block_mul_ij"> <goal name="VC block_mul_ij" expl="VC for block_mul_ij">
<proof prover="2"><result status="valid" time="0.47" steps="452"/></proof> <transf name="split_goal_wp">
<goal name="VC block_mul_ij.1" expl="1. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.08" steps="79"/></proof>
</goal>
<goal name="VC block_mul_ij.2" expl="2. variant decrease">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.3" expl="3. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.4" expl="4. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.5" expl="5. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC block_mul_ij.6" expl="6. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.20" steps="118"/></proof>
</goal>
<goal name="VC block_mul_ij.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="1.48"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="WP_parameter mul_split" expl="VC for mul_split"> <goal name="VC mul_split" expl="VC for mul_split">
<proof prover="2"><result status="valid" time="0.29" steps="363"/></proof> <transf name="split_goal_wp">
<goal name="VC mul_split.1" expl="1. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC mul_split.2" expl="2. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC mul_split.3" expl="3. precondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC mul_split.4" expl="4. assertion">
<proof prover="2" timelimit="1"><result status="valid" time="0.20" steps="317"/></proof>
</goal>
<goal name="VC mul_split.5" expl="5. postcondition">
<proof prover="2" timelimit="1"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
</transf>
</goal> </goal>
<goal name="WP_parameter mul_block_cell" expl="VC for mul_block_cell"> <goal name="VC mul_block_cell" expl="VC for mul_block_cell">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter mul_block_cell.1" expl="1. precondition"> <goal name="VC mul_block_cell.1" expl="1. precondition">
<proof prover="2"><result status="valid" time="0.03" steps="28"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.03" steps="28"/></proof>
</goal> </goal>
<goal name="WP_parameter mul_block_cell.2" expl="2. postcondition"> <goal name="VC mul_block_cell.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.12" steps="136"/></proof> <proof prover="2" timelimit="1"><result status="valid" time="0.13" steps="136"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -312,12 +312,6 @@ module Symb ...@@ -312,12 +312,6 @@ module Symb
predicate (-->) (x y:'a) = "rewrite" x = y predicate (-->) (x y:'a) = "rewrite" x = y
meta rewrite_def predicate (-->) meta rewrite_def predicate (-->)
predicate (--->) (x y:expr) =
x.e_body --> y.e_body /\
x.e_rows --> y.e_rows /\
x.e_cols --> y.e_cols
meta rewrite_def predicate (--->)
predicate e_vld (env:env) (e:expr) = predicate e_vld (env:env) (e:expr) =
e.e_rows >= 0 /\ e.e_cols >= 0 /\ e.e_rows >= 0 /\ e.e_cols >= 0 /\
LOCAL.lm_vld env.ev_f e.e_rows e.e_cols e.e_body LOCAL.lm_vld env.ev_f e.e_rows e.e_cols e.e_body
...@@ -344,7 +338,7 @@ module Symb ...@@ -344,7 +338,7 @@ module Symb
writes { env } writes { env }
ensures { env.ev_c --> old env.ev_c + 1 } ensures { env.ev_c --> old env.ev_c + 1 }
ensures { env.ev_f --> extends (old env.ev_f) (old env.ev_c) m } ensures { env.ev_f --> extends (old env.ev_f) (old env.ev_c) m }
ensures { result ---> symb_mat m (old env.ev_c) } ensures { result --> symb_mat m (old env.ev_c) }
ensures { e_vld env result } ensures { e_vld env result }
= let id = env.ev_c in = let id = env.ev_c in
env.ev_f <- extends env.ev_f id m; env.ev_c <- id + 1; env.ev_f <- extends env.ev_f id m; env.ev_c <- id + 1;
...@@ -357,7 +351,7 @@ module Symb ...@@ -357,7 +351,7 @@ module Symb
let ghost symb_opp (env:env) (e:expr) : expr let ghost symb_opp (env:env) (e:expr) : expr
requires { e_vld env e } requires { e_vld env e }
ensures { e_vld env result } ensures { e_vld env result }
ensures { result ---> symb_opp e } ensures { result --> symb_opp e }
ensures { e_mdl env result = opp (e_mdl env e) } ensures { e_mdl env result = opp (e_mdl env e) }
= let (r,c) = (e.e_rows,e.e_cols) in = let (r,c) = (e.e_rows,e.e_cols) in
LOCAL.lm_mdl_same env.ev_f r c e.e_body; LOCAL.lm_mdl_same env.ev_f r c e.e_body;
...@@ -375,7 +369,7 @@ module Symb ...@@ -375,7 +369,7 @@ module Symb
requires { e_vld env e1 /\ e_vld env e2 } requires { e_vld env e1 /\ e_vld env e2 }
requires { e1.e_rows = e2.e_rows /\ e1.e_cols = e2.e_cols } requires { e1.e_rows = e2.e_rows /\ e1.e_cols = e2.e_cols }
ensures { e_vld env result } ensures { e_vld env result }
ensures { result ---> symb_add e1 e2 } ensures { result --> symb_add e1 e2 }
ensures { e_mdl env result = add (e_mdl env e1) (e_mdl env e2) } ensures { e_mdl env result = add (e_mdl env e1) (e_mdl env e2) }
= let (r,c) = (e1.e_rows, e1.e_cols) in = let (r,c) = (e1.e_rows, e1.e_cols) in
LOCAL.lm_mdl_same env.ev_f r c e1.e_body; LOCAL.lm_mdl_same env.ev_f r c e1.e_body;
...@@ -393,7 +387,7 @@ module Symb ...@@ -393,7 +387,7 @@ module Symb
requires { e_vld env e1 /\ e_vld env e2 } requires { e_vld env e1 /\ e_vld env e2 }
requires { e1.e_rows = e2.e_rows /\ e1.e_cols = e2.e_cols } requires { e1.e_rows = e2.e_rows /\ e1.e_cols = e2.e_cols }
ensures { e_vld env result } ensures { e_vld env result }
ensures { result ---> symb_sub e1 e2 } ensures { result --> symb_sub e1 e2 }
ensures { e_mdl env result = sub (e_mdl env e1) (e_mdl env e2) } ensures { e_mdl env result = sub (e_mdl env e1) (e_mdl env e2) }
= symb_add env e1 (symb_opp env e2) = symb_add env e1 (symb_opp env e2)
...@@ -406,7 +400,7 @@ module Symb ...@@ -406,7 +400,7 @@ module Symb
requires { e_vld env e1 /\ e_vld env e2 } requires { e_vld env e1 /\ e_vld env e2 }
requires { e1.e_cols = e2.e_rows } requires { e1.e_cols = e2.e_rows }
ensures { e_vld env result } ensures { e_vld env result }
ensures { result ---> symb_mul e1 e2 } ensures { result --> symb_mul e1 e2 }
ensures { e_mdl env result = mul (e_mdl env e1) (e_mdl env e2) } ensures { e_mdl env result = mul (e_mdl env e1) (e_mdl env e2) }
= let (r,k,c) = (e1.e_rows,e1.e_cols,e2.e_cols) in = let (r,k,c) = (e1.e_rows,e1.e_cols,e2.e_cols) in
LOCAL.lm_mdl_same env.ev_f r k e1.e_body; LOCAL.lm_mdl_same env.ev_f r k e1.e_body;
......
...@@ -2,85 +2,76 @@ ...@@ -2,85 +2,76 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../naive.mlw"> <file name="../naive.mlw">
<theory name="MatrixMultiplication" sum="888d777f6b0bead427ee1083245abb55"> <theory name="MatrixMultiplication" sum="911c4e0a5b3fe8cc6dacaa3acb684928">
<goal name="WP_parameter mult_naive" expl="VC for mult_naive"> <goal name="VC mult_naive" expl="VC for mult_naive">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter mult_naive.1" expl="1. precondition"> <goal name="VC mult_naive.1" expl="1. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.2" expl="2. postcondition"> <goal name="VC mult_naive.2" expl="2. loop bounds">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.3" expl="3. postcondition"> <goal name="VC mult_naive.3" expl="3. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.4" expl="4. loop invariant init"> <goal name="VC mult_naive.4" expl="4. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.5" expl="5. loop invariant init"> <goal name="VC mult_naive.5" expl="5. loop bounds">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.6" expl="6. loop invariant preservation"> <goal name="VC mult_naive.6" expl="6. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.7" expl="7. loop invariant preservation"> <goal name="VC mult_naive.7" expl="7. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="21"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.8" expl="8. loop invariant init"> <goal name="VC mult_naive.8" expl="8. loop bounds">
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.9" expl="9. loop invariant preservation"> <goal name="VC mult_naive.9" expl="9. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.10" expl="10. loop invariant preservation"> <goal name="VC mult_naive.10" expl="10. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.11" expl="11. loop invariant init"> <goal name="VC mult_naive.11" expl="11. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="17"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.12" expl="12. index in array bounds"> <goal name="VC mult_naive.12" expl="12. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter mult_naive.13" expl="13. index in array bounds">
<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="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="1"><result status="valid" time="0.01" steps="26"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.16" expl="16. index in array bounds"> <goal name="VC mult_naive.13" expl="13. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.17" expl="17. loop invariant preservation"> <goal name="VC mult_naive.14" expl="14. index in matrix bounds">
<proof prover="1"><result status="valid" time="0.03" steps="41"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="17"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.18" expl="18. loop invariant preservation"> <goal name="VC mult_naive.15" expl="15. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.06" steps="56"/></proof> <proof prover="1"><result status="valid" time="0.03" steps="31"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.19" expl="19. loop invariant preservation"> <goal name="VC mult_naive.16" expl="16. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="24"/></proof> <proof prover="1"><result status="valid" time="0.09" steps="77"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.20" expl="20. loop invariant preservation"> <goal name="VC mult_naive.17" expl="17. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="23"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="21"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.21" expl="21. loop invariant preservation"> <goal name="VC mult_naive.18" expl="18. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.22" expl="22. loop invariant preservation"> <goal name="VC mult_naive.19" expl="19. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.03" steps="40"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="28"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.23" expl="23. type invariant"> <goal name="VC mult_naive.20" expl="20. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="1"><result status="valid" time="0.01" steps="52"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.24" expl="24. postcondition"> <goal name="VC mult_naive.21" expl="21. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal> </goal>
<goal name="WP_parameter mult_naive.25" expl="25. postcondition"> <goal name="VC mult_naive.22" expl="22. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="20"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="14"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -40,16 +40,8 @@ module MatrixMultiplication ...@@ -40,16 +40,8 @@ module MatrixMultiplication
done; done;
done done
function mdl (m: matrix 'a) : mat 'a = let ghost function mdl (m: matrix 'a) : mat {'a} =
create m.rows m.columns (fun i j -> get m i j) create m.rows m.columns m.elts
(*** Very technical: Why3 refuses calls to logic functions
in programs when the function signature contains impure types
(e.g like matrix 'a). However, this is safe for the particular
case of functions that project an impure type to a pure one, so we
assume it is possible. *)
val ghost mdl (m:matrix 'a) : mat 'a
ensures { result = mdl m }
type with_symb = { type with_symb = {
phy : matrix int; phy : matrix int;
...@@ -77,8 +69,8 @@ module MatrixMultiplication ...@@ -77,8 +69,8 @@ module MatrixMultiplication
requires { 0 <= c <= c + dc <= a.mdl.F.cols } requires { 0 <= c <= c + dc <= a.mdl.F.cols }
ensures { let rm = result.phy.mdl in ensures { let rm = result.phy.mdl in
rm = block a.mdl r dr c dc /\ rm.F.rows = dr /\ rm.F.cols = dc } rm = block a.mdl r dr c dc /\ rm.F.rows = dr /\ rm.F.cols = dc }
ensures { result.sym ---> symb_mat result.phy.mdl (old env.ev_c) } ensures { result.sym --> symb_mat result.phy.mdl (old env.ev_c) }
ensures { env.ev_f --> old (extends env.ev_f env.ev_c result.phy.mdl) } ensures { env.ev_f --> extends (old env.ev_f) (old env.ev_c) result.phy.mdl }
ensures { env.ev_c --> old env.ev_c + 1 } ensures { env.ev_c --> old env.ev_c + 1 }
ensures { with_symb_vld env result } ensures { with_symb_vld env result }
= let m = block a r dr c dc in = let m = block a r dr c dc in
...@@ -109,7 +101,7 @@ module MatrixMultiplication ...@@ -109,7 +101,7 @@ module MatrixMultiplication
requires { a.phy.mdl === b.phy.mdl } requires { a.phy.mdl === b.phy.mdl }
requires { with_symb_vld env a /\ with_symb_vld env b } requires { with_symb_vld env a /\ with_symb_vld env b }
ensures { result.phy.mdl = add a.phy.mdl b.phy.mdl } ensures { result.phy.mdl = add a.phy.mdl b.phy.mdl }
ensures { result.sym ---> symb_add a.sym b.sym } ensures { result.sym --> symb_add a.sym b.sym }
ensures { with_symb_vld env result } ensures { with_symb_vld env result }
= { phy = add a.phy b.phy; = { phy = add a.phy b.phy;
sym = ghost symb_add env a.sym b.sym } sym = ghost symb_add env a.sym b.sym }
...@@ -138,7 +130,7 @@ module MatrixMultiplication ...@@ -138,7 +130,7 @@ module MatrixMultiplication
requires { a.phy.mdl === b.phy.mdl } requires { a.phy.mdl === b.phy.mdl }
requires { with_symb_vld env a /\ with_symb_vld env b } requires { with_symb_vld env a /\ with_symb_vld env b }
ensures { result.phy.mdl = sub a.phy.mdl b.phy.mdl } ensures { result.phy.mdl = sub a.phy.mdl b.phy.mdl }
ensures { result.sym ---> symb_sub a.sym b.sym } ensures { result.sym --> symb_sub a.sym b.sym }
ensures { with_symb_vld env result } ensures { with_symb_vld env result }
= { phy = sub a.phy b.phy; = { phy = sub a.phy b.phy;
sym = ghost symb_sub env a.sym b.sym } sym = ghost symb_sub env a.sym b.sym }
...@@ -169,7 +161,7 @@ module MatrixMultiplication ...@@ -169,7 +161,7 @@ module MatrixMultiplication
invariant { forall i0 j0. 0 <= i0 < r /\ 0 <= j0 < c /\ invariant { forall i0 j0. 0 <= i0 < r /\ 0 <= j0 < c /\
(i0 <> i \/ j0 <> j) -> (i0 <> i \/ j0 <> j) ->
rs.elts[i0][j0] = (rs at I).elts[i0][j0] } rs.elts[i0][j0] = (rs at I).elts[i0][j0] }
invariant { rs.elts[i][j] = sum 0 k (mul_atom a.mdl b.mdl i j) } invariant { rs.elts[i][j] = sum (mul_atom a.mdl b.mdl i j) 0 k }
set rs i j (get rs i j + get a i k * get b k j) set rs i j (get rs i j + get a i k * get b k j)
done done
done; done;
...@@ -196,14 +188,14 @@ module MatrixMultiplication ...@@ -196,14 +188,14 @@ module MatrixMultiplication
invariant { forall i0 j0. 0 <= i0 < r /\ 0 <= j0 < c /\ i0 <> i -> invariant { forall i0 j0. 0 <= i0 < r /\ 0 <= j0 < c /\ i0 <> i ->
rs.elts[i0][j0] = (rs at M).elts[i0][j0] } rs.elts[i0][j0] = (rs at M).elts[i0][j0] }
invariant { forall j0. 0 <= j0 < c -> invariant { forall j0. 0 <= j0 < c ->
rs.elts[i][j0] = sum 0 k (mul_atom a.mdl b.mdl i j0) } rs.elts[i][j0] = sum (mul_atom a.mdl b.mdl i j0) 0 k }
label I in label I in
for j = 0 to c - 1 do for j = 0 to c - 1 do
invariant { forall i0 j0. invariant { forall i0 j0.
0 <= i0 < r /\ 0 <= j0 < c /\ (i0 <> i \/ j0 >= j) -> 0 <= i0 < r /\ 0 <= j0 < c /\ (i0 <> i \/ j0 >= j) ->
rs.elts[i0][j0] = (rs at I).elts[i0][j0] } rs.elts[i0][j0] = (rs at I).elts[i0][j0] }
invariant { forall j0. 0 <= j0 < j -> invariant { forall j0. 0 <= j0 < j ->
rs.elts[i][j0] = sum 0 (k+1) (mul_atom a.mdl b.mdl i j0) } rs.elts[i][j0] = sum (mul_atom a.mdl b.mdl i j0) 0 (k+1) }
set rs i j (get rs i j + get a i k * get b k j) set rs i j (get rs i j + get a i k * get b k j)
done; done;
done; done;
...@@ -319,7 +311,7 @@ module MatrixMultiplication ...@@ -319,7 +311,7 @@ module MatrixMultiplication
requires { b.phy.mdl.F.rows = qm /\ b.phy.mdl.F.cols = qc } requires { b.phy.mdl.F.rows = qm /\ b.phy.mdl.F.cols = qc }