Skip to content

GitLab

why3
why3
Commit a6b2eab2 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

updated proof sessions

parent 48ab8464
Hide whitespace changes
Inline Side-by-side
Showing with 44 additions and 38 deletions
examples/programs/isqrt/why3session.xml
View file @ a6b2eab2
......@@ -3,15 +3,15 @@
<why3session name="examples/programs/isqrt/why3session.xml">
<file name="../isqrt.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="5c9a0a28616c8a34d7fb4e3e77a12070" proved="true" expanded="true">
<goal name="WP_parameter isqrt" expl="correctness of parameter isqrt" sum="71cc23114951a4ecb6b4f3257d65e891" proved="true" expanded="true">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter main" expl="correctness of parameter main" sum="7960ecfe2bbd563711f4786261fcb516" proved="true" expanded="true">
<goal name="WP_parameter main" expl="correctness of parameter main" sum="1c68d9c3079316cc99cf2e1bf49cbce6" proved="true" expanded="true">
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......
examples/programs/list_rev/why3session.xml
View file @ a6b2eab2
......@@ -3,67 +3,76 @@
<why3session name="examples/programs/list_rev/why3session.xml">
<file name="../list_rev.mlw" verified="false" expanded="true">
<theory name="WP M" verified="false" expanded="true">
<goal name="acyclic_list" sum="05ff1ad20f5af90fc986f7d1deb8acbf" proved="false" expanded="true">
<goal name="acyclic_list" sum="7db83a937373a8239579a364820ee4d2" proved="false" expanded="true">
</goal>
<goal name="consistent" sum="678d57b4a5464ed1788c9284cd3deb14" proved="false" expanded="true">
<goal name="consistent" sum="590df07cf83264b32e414a773bbd0a39" proved="false" expanded="true">
</goal>
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="1ed3408e037f1f79e9735208d22637d9" proved="true" expanded="true">
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="57202003173952c9ba4cc18145406ac0" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal name="reverse_append" sum="95eaedbd88c6733c31f6f90543952407" proved="false" expanded="true">
<goal name="reverse_append" sum="5e1e29aaddde77691465057e4c33dc3b" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="4087cd4ed78b8c5468550eec66d4564d" proved="false" expanded="true">
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="6165c919ade606c3dae98f331b0e999f" proved="false" expanded="true">
</goal>
</theory>
<theory name="WP M2" verified="false" expanded="true">
<goal name="is_list_disjoint_case" sum="db8d14254ea7d12f7f7bbb446ee006eb" proved="true" expanded="true">
<goal name="is_list_disjoint_case" sum="68e81e53620d2aa65d9c0628265ca99b" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="frame_list" sum="bb671f60ef471cba398e52a876544a54" proved="true" expanded="true">
<goal name="frame_list" sum="25b6e77de519460237f6947621f25a0d" proved="true" expanded="false">
<proof prover="coq" timelimit="10" edited="list_rev_M2_frame_list_1.v" obsolete="false">
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal name="frame_list_ft" sum="d0c0dd407e6667c967cd37f14169af5e" proved="true" expanded="true">
<goal name="frame_list_ft" sum="4db7a9d330284b5bd6ca63f01f9a8120" proved="true" expanded="false">
<proof prover="coq" timelimit="10" edited="list_rev_M2_frame_list_ft_1.v" obsolete="false">
<result status="valid" time="0.54"/>
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal name="acyclic_list" sum="9beb2427d92c0d05c7ab34738d84fb20" proved="false" expanded="true">
<goal name="acyclic_list" sum="394041341bfca1932823e503c766930a" proved="false" expanded="true">
</goal>
<goal name="consistent" sum="c4812a324be896e9f0a42c752b48a304" proved="false" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<goal name="consistent" sum="a65f10bfef659ef89fea02a802b02814" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.10"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.03"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof prover="spass" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.11"/>
</proof>
</goal>
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="2cf5c0afcc43f0a5bf2667c7c738c555" proved="true" expanded="true">
<goal name="WP_parameter list_rev" expl="correctness of parameter list_rev" sum="17367e075517f9d5ea5ccf101b9e17ae" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="frame_model" sum="d5fd36bbd6e0e2aebeea5703bbf7b4d7" proved="true" expanded="true">
<goal name="frame_model" sum="0110aae7bb2d45d63dfe5adf4ca21c97" proved="true" expanded="false">
<proof prover="coq" timelimit="10" edited="list_rev_M2_frame_model_1.v" obsolete="false">
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal name="consistent_behv" sum="f9e3c4ba36897ccd68e9407e528ff384" proved="false" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<goal name="consistent_behv" sum="241d74963c5ce2c9219d0047e431cd78" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="0.10"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.04"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<proof prover="spass" timelimit="10" edited="" obsolete="true">
<result status="timeout" time="10.05"/>
</proof>
</goal>
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="52a60a766a87079ec4ccbf52ed6012eb" proved="true" expanded="true">
<goal name="WP_parameter list_rev_behv" expl="correctness of parameter list_rev_behv" sum="44044f62ee75d1bc2024edb4518ff0d5" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.18"/>
<result status="valid" time="0.14"/>
</proof>
</goal>
</theory>
......
examples/programs/vacid_0_sparse_array.mlw
View file @ a6b2eab2
......@@ -87,6 +87,9 @@ back +-+-+-+-------------------+
a.card = a.length ->
forall i: int. 0 <= i < a.length -> is_elt a i
lemma permutation2 :
false
let set (a: sparse_array 'a) i v =
{ 0 <= i < length a /\ sa_inv a }
a.values[i] <- v;
......
examples/programs/vacid_0_sparse_array/why3session.xml
View file @ a6b2eab2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/vacid_0_sparse_array/why3session.xml">
<file name="../vacid_0_sparse_array.mlw" verified="true" expanded="true">
<theory name="WP SparseArray" verified="true" expanded="true">
<file name="../vacid_0_sparse_array.mlw" verified="false" expanded="true">
<theory name="WP SparseArray" verified="false" expanded="true">
<goal name="WP_parameter create" expl="normal postcondition" sum="a5cf0ebd4e044474e9354356099a0e63" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
......@@ -18,13 +18,7 @@
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="permutation" sum="786f5a179e9e8690bc48d4028698bcda" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
</proof>
<proof prover="yices" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<goal name="permutation" sum="786f5a179e9e8690bc48d4028698bcda" proved="false" expanded="true">
</goal>
<goal name="WP_parameter set" expl="correctness of parameter set" sum="e41489f0bcf26e9a442362dd75a26152" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
......
examples/scottish-private-club/why3session.xml
View file @ a6b2eab2
......@@ -3,18 +3,18 @@
<why3session name="examples/scottish-private-club/why3session.xml">
<file name="../scottish-private-club.why" verified="true" expanded="true">
<theory name="ScottishClubProblem" verified="true" expanded="true">
<goal name="ThereIsNobodyInTheClub" sum="fdd6f04d95bf043a8b2934a2bd2c47ad" proved="true" expanded="true">
<goal name="ThereIsNobodyInTheClub" sum="c3a407614cecf50c38f66fddd8e677f5" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
......
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