Skip to content

GitLab

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

two more programs for the nightly bench

parent acff993f
Hide whitespace changes
Inline Side-by-side
Showing with 120 additions and 26 deletions
.gitignore
View file @ 1c47e80c
......@@ -152,7 +152,6 @@ why.conf
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/binary_search2/
/examples/programs/vacid_0_sparse_array/
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
......@@ -160,7 +159,6 @@ why.conf
/examples/programs/vstte10_search_list/
/examples/programs/vstte10_aqueue/
/examples/programs/mergesort_list/
/examples/programs/same_fringe/
/examples/programs/algo63/
/examples/programs/algo64/
/examples/programs/algo65/
......
examples/programs/same_fringe/why3session.xml 0 → 100644
View file @ 1c47e80c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/same_fringe/why3session.xml">
<file name="../same_fringe.mlw" verified="true" expanded="true">
<theory name="SameFringe" verified="true" expanded="true">
<goal name="WP_enum" expl="correctness of enum" sum="a88e6bbf942db53576d5061640c13823" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.64"/>
</proof>
</goal>
<goal name="WP_eq_enum" expl="correctness of eq_enum" sum="11a451fdc4d6ebb10c4d89b5081d5aa9" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_same_fringe" expl="normal postcondition" sum="aab1ac13bc5135eb61f706e2989a61b0" proved="true" expanded="true">
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/programs/vacid_0_sparse_array.mlw
View file @ 1c47e80c
......@@ -93,10 +93,7 @@ back +-+-+-+-------------------+
let test (a: sparse_array) i =
{ 0 <= i < length a and invariant_ a }
let idx = idx a in
let back = back a in
let n = card a in
0 <= idx[i] && idx[i] < n && back[idx[i]] = i
0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i
{ result=True <-> is_elt a i }
let get (a: sparse_array) i =
......@@ -109,17 +106,12 @@ back +-+-+-+-------------------+
let set (a: sparse_array) i v =
{ 0 <= i < length a and invariant_ a }
(* let SA val idx back sz n = !a in *)
let val = val a in
let idx = idx a in
let back = back a in
let n = card a in
val[i] <- v;
a.val[i] <- v;
if not (test a i) then begin
assert { n < length a };
idx[i] <- n;
back[n] <- i;
() (*TODO a.card <- n+1 *)
assert { a.card < length a };
a.idx[i] <- a.card;
a.back[a.card] <- i;
a.card <- a.card + 1
end
{ invariant_ a and
model a i = v and
......
examples/programs/vacid_0_sparse_array/why3session.xml 0 → 100644
View file @ 1c47e80c
<?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="M" verified="true" expanded="true">
<goal name="Inter6" sum="0727b5a4a322503f1341f4fbd4411a08" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter create" expl="normal postcondition" sum="a72f8526348fcdf26ba9f3c960e50161" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal name="WP_parameter test" expl="correctness of parameter test" sum="46b3233ebb601f30c1048306394e9fae" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal name="WP_parameter get" expl="correctness of parameter get" sum="c274083105ab3c9b6d8c5ed773227cfe" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.09"/>
</proof>
</goal>
<goal name="WP_parameter set" expl="correctness of parameter set" sum="abc4fbc70002208565dc51236d9434eb" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.32"/>
</proof>
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter set.1" expl="precondition" sum="e97e9180e4686a3a0621e79128b8756c" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter set.2" expl="precondition" sum="f8ba3eb882368987dc3e24fdedc87779" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.61"/>
</proof>
</goal>
<goal name="WP_parameter set.3" expl="assertion" sum="717c232a57062bc91e4ecc2a714c0930" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal name="WP_parameter set.4" expl="precondition" sum="f818511062f21645e10c65e596841e52" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="WP_parameter set.5" expl="precondition" sum="f184dce4ff165fdd818097d0f450cc57" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal name="WP_parameter set.6" expl="normal postcondition" sum="b59d8de2bc15422d729dec7fc7c3aa19" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="5.92"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.07"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.82"/>
</proof>
</goal>
<goal name="WP_parameter set.7" expl="normal postcondition" sum="71fd27d9c63afe486a3891e68e6381b1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.59"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter harness" expl="correctness of parameter harness" sum="2fb6b907ff76117a129f96aa79af8cc4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="4.44"/>
</proof>
</goal>
</theory>
</file>
</why3session>
examples/programs/zeros/why3session.xml
View file @ 1c47e80c
......@@ -3,19 +3,19 @@
<why3session name="examples/programs/zeros/why3session.xml">
<file name="../zeros.mlw" verified="true" expanded="true">
<theory name="SetZeros" verified="true" expanded="true">
<goal name="WP_parameter set_zeros" expl="correctness of parameter set_zeros" sum="738a61fe56ee3528c88f7f6ad392b4ec" proved="true" expanded="true">
<goal name="WP_parameter set_zeros" expl="correctness of parameter set_zeros" sum="61eb8ab27b075cc9f9557662701deb9a" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.1" expl="normal postcondition" sum="5ebaf8196c461842d3818d0f00c7b897" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.1" expl="normal postcondition" sum="9934ac330413647e3ce065099e571460" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.2" expl="for loop initialization" sum="262d92c8877fa84a114fda64ce36167b" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.2" expl="for loop initialization" sum="c54bdc4d37361cc9832d507f67389c90" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.3" expl="for loop preservation" sum="db37970e847fa3b97df4a7062a16ffea" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.3" expl="for loop preservation" sum="ab559f2cafe67190b6b0fdc52183acf0" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
......@@ -23,24 +23,24 @@
<result status="unknown" time="0.02"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter set_zeros.4" expl="normal postcondition" sum="e37d7aade59a72a7fadbab4f042fdec6" proved="true" expanded="true">
<goal name="WP_parameter set_zeros.4" expl="normal postcondition" sum="27a169d744fee28adaefe96cd86be7b4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter harness" expl="correctness of parameter harness" sum="063941a2fece0c3d9083e25e9187d847" proved="true" expanded="true">
<goal name="WP_parameter harness" expl="correctness of parameter harness" sum="71fe54e578e1a17eae1ad025f530eda9" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter harness.1" expl="assertion" sum="d48c1f007a0cb3fcb8c7c2072af4f1b2" proved="true" expanded="true">
<goal name="WP_parameter harness.1" expl="assertion" sum="93146ed254dd825c0ac00dbb2643b96d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter harness.2" expl="assertion" sum="6cd977227d738cbea667ca77e1839b1c" proved="true" expanded="true">
<goal name="WP_parameter harness.2" expl="assertion" sum="8369f550814b2c44e0725ba455737dd4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
......
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