updated proof sessions

parent d98661f6
......@@ -4,7 +4,6 @@ bignum.mlw
bitcount.mlw
bitvector_examples.mlw
bitwalker.mlw
coincidence_count_list.mlw
counting_sort.mlw
cursor.mlw
dijkstra.mlw
......@@ -13,10 +12,6 @@ ewd673.mlw
fibonacci.mlw
find.mlw
finite_tarski.mlw
flag2.mlw
foveoos11_challenge1.mlw
foveoos11_challenge2.mlw
foveoos11_challenge3.mlw
gcd_bezout.mlw
gcd.mlw
hackers-delight.mlw
......
......@@ -2,120 +2,30 @@
<!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="6" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coincidence_count_list.mlw" expanded="true">
<theory name="CoincidenceCount" sum="9a0ad21c9ece5af6e3bf77ad2c0d1d81">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<theory name="CoincidenceCount" sum="905b884a839c618907ffebe24b767896" expanded="true">
<goal name="Transitive.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
<transf name="split_goal_wp">
<goal name="WP_parameter coincidence_count.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.82" steps="2661"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="1.24" steps="3244"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="2.71" steps="6776"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. postcondition">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
<goal name="VC coincidence_count" expl="VC for coincidence_count" expanded="true">
<proof prover="2"><result status="valid" time="2.20" steps="9859"/></proof>
</goal>
</theory>
<theory name="CoincidenceCountAnyType" sum="2effd4ea5f064da956ab4d367f092582">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
<theory name="CoincidenceCountAnyType" sum="a063592bd4e78e3599214a54a49c4910" expanded="true">
<goal name="Transitive.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
<proof prover="0"><result status="valid" time="3.63" steps="12168"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter coincidence_count.1" expl="1. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.4" expl="4. postcondition">
<proof prover="0"><result status="valid" time="0.57" steps="2400"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.5" expl="5. variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.36" steps="1750"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.9" expl="9. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.10" expl="10. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.11" expl="11. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="0.52" steps="1823"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.13" expl="13. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="WP_parameter coincidence_count.14" expl="14. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
</transf>
<goal name="VC coincidence_count" expl="VC for coincidence_count">
<proof prover="2"><result status="valid" time="0.65" steps="4194"/></proof>
</goal>
</theory>
<theory name="CoincidenceCountList" sum="66d71efd5b320baab93930df25784477">
<goal name="Transitive.Trans">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
<theory name="CoincidenceCountList" sum="e75739bbd76111eb2670e596d18c2279" expanded="true">
<goal name="Transitive.Trans" expanded="true">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="WP_parameter coincidence_count" expl="VC for coincidence_count">
<proof prover="0"><result status="valid" time="0.24" steps="657"/></proof>
<goal name="VC coincidence_count" expl="VC for coincidence_count">
<proof prover="2"><result status="valid" time="0.15" steps="1000"/></proof>
</goal>
</theory>
</file>
......
This diff is collapsed.
......@@ -19,65 +19,69 @@ module Flag
| _,_ -> False
end
predicate monochrome (a:map int color) (i:int) (j:int) (c:color) =
forall k:int. i <= k < j -> a[k]=c
predicate monochrome (a: map int color) (i: int) (j: int) (c: color) =
forall k: int. i <= k < j -> a[k]=c
let rec function nb_occ (a:map int color) (i:int) (j:int) (c:color) : int
let rec function nb_occ (a: map int color) (i: int) (j: int) (c: color) : int
variant { j - i }
= if i >= j then 0 else
if eq_color a[j-1] c then 1 + nb_occ a i (j-1) c else nb_occ a i (j-1) c
let rec lemma nb_occ_split (a:map int color) (i j k:int) (c:color)
let rec lemma nb_occ_split (a: map int color) (i j k: int) (c: color)
requires { i <= j <= k }
variant { k - j }
ensures { nb_occ a i k c = nb_occ a i j c + nb_occ a j k c }
= if k = j then () else nb_occ_split a i j (k-1) c
let rec lemma nb_occ_ext (a1 a2:map int color) (i j:int) (c:color)
requires { forall k:int. i <= k < j -> a1[k] = a2[k] }
let rec lemma nb_occ_ext (a1 a2: map int color) (i j: int) (c: color)
requires { forall k: int. i <= k < j -> a1[k] = a2[k] }
variant { j - i }
ensures { nb_occ a1 i j c = nb_occ a2 i j c }
= if i >= j then () else nb_occ_ext a1 a2 i (j-1) c
lemma nb_occ_store_outside_up:
forall a:map int color, i j k:int, c:color.
forall a: map int color, i j k: int, c: color.
i <= j <= k -> nb_occ (set a k c) i j c = nb_occ a i j c
lemma nb_occ_store_outside_down:
forall a:map int color, i j k:int, c:color.
forall a: map int color, i j k: int, c: color.
k < i <= j -> nb_occ (set a k c) i j c = nb_occ a i j c
lemma nb_occ_store_eq_eq:
forall a:map int color, i j k:int, c:color.
forall a: map int color, i j k: int, c: color.
i <= k < j -> a[k] = c ->
nb_occ (set a k c) i j c = nb_occ a i j c
let rec lemma nb_occ_store_eq_neq (a:map int color) (i j k:int) (c:color)
let rec lemma nb_occ_store_eq_neq (a: map int color) (i j k: int) (c: color)
requires { i <= k < j }
requires { a[k] <> c }
variant { j - k }
ensures { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
variant { j - k }
ensures { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
= if k = j - 1 then () else nb_occ_store_eq_neq a i (j-1) k c
lemma nb_occ_store_neq_eq:
forall a:map int color, i j k:int, c c':color.
i <= k < j -> c <> c' -> a[k] = c ->
nb_occ (set a k c') i j c = nb_occ a i j c - 1
let lemma nb_occ_store_neq_eq
(a: map int color) (i j k: int) (c c': color)
requires { i <= k < j } requires { c <> c' } requires { a[k] = c }
ensures { nb_occ (set a k c') i j c = nb_occ a i j c - 1 }
= nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
lemma nb_occ_store_neq_neq:
forall a:map int color, i j k:int, c c':color.
i <= k < j -> c <> c' -> a[k] <> c ->
nb_occ (set a k c') i j c = nb_occ a i j c
let lemma nb_occ_store_neq_neq
(a: map int color) (i j k: int) (c c': color)
requires { i <= k < j } requires { c <> c' } requires { a[k] <> c }
ensures { nb_occ (set a k c') i j c = nb_occ a i j c }
= nb_occ_split a i k j c; nb_occ_split (set a k c') i k j c;
nb_occ_split a k (k + 1) j c; nb_occ_split (set a k c') k (k+1) j c
use import array.Array
let swap (a:array color) (i:int) (j:int) : unit
let swap (a:array color) (i: int) (j: int) : unit
requires { 0 <= i < a.length }
requires { 0 <= j < a.length }
ensures { a[i] = old a[j] }
ensures { a[j] = old a[i] }
ensures { forall k:int. k <> i /\ k <> j -> a[k] = old a[k] }
ensures { forall k1 k2:int, c:color. k1 <= i < k2 /\ k1 <= j < k2 ->
ensures { forall k: int. k <> i /\ k <> j -> a[k] = old a[k] }
ensures { forall k1 k2: int, c: color. k1 <= i < k2 /\ k1 <= j < k2 ->
nb_occ a.elts k1 k2 c = nb_occ (old a.elts) k1 k2 c }
= let ai = a[i] in
let aj = a[j] in
......@@ -86,11 +90,11 @@ module Flag
let dutch_flag (a:array color)
ensures { (exists b:int. exists r:int.
ensures { (exists b: int. exists r: int.
monochrome a.elts 0 b Blue /\
monochrome a.elts b r White /\
monochrome a.elts r a.length Red) }
ensures { forall c:color.
ensures { forall c: color.
nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
= let b = ref 0 in
let i = ref 0 in
......@@ -101,7 +105,7 @@ module Flag
invariant { monochrome a.elts !b !i White }
invariant { monochrome a.elts !r a.length Red }
invariant {
forall c:color.
forall c: color.
nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
variant { !r - !i }
match a[!i] with
......
This diff is collapsed.
......@@ -2,48 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../foveoos11_challenge1.mlw" expanded="true">
<theory name="Max" sum="4d062e300c422dd912abe62a0612e474" expanded="true">
<goal name="WP_parameter max" expl="VC for max" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter max.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter max.2" expl="2. loop invariant init">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter max.3" expl="3. index in array bounds">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="WP_parameter max.4" expl="4. index in array bounds">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter max.5" expl="5. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter max.7" expl="7. loop variant decrease">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.8" expl="8. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.9" expl="9. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter max.10" expl="10. loop variant decrease">
<proof prover="1" timelimit="10" memlimit="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter max.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="WP_parameter max.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
<theory name="Max" sum="d07f3e92fc559af0ac7bb5338d945993" expanded="true">
<goal name="VC max" expl="VC for max" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,15 +2,15 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../foveoos11_challenge2.mlw" expanded="true">
<theory name="MaximumTree" sum="a00e1f9c636259085c5337c363a52ea1" expanded="true">
<theory name="MaximumTree" sum="fce5c2a3c40462a4ace022ab88c3a4e9" expanded="true">
<goal name="size_nonneg" expanded="true">
<proof prover="0" edited="foveoos11_challenge2_WP_MaximumTree_size_nonneg_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="WP_parameter maximum" expl="VC for maximum" expanded="true">
<proof prover="2"><result status="valid" time="0.56" steps="812"/></proof>
<goal name="VC maximum" expl="VC for maximum" expanded="true">
<proof prover="1"><result status="valid" time="0.25" steps="1474"/></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