Skip to content

GitLab

Commit 6ee33b56 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Merge branch 'new_system' into negative_literals

parents ed83395f da4b2a00
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 529 additions and 500 deletions
Makefile.in
View file @ 6ee33b56
......@@ -1608,7 +1608,7 @@ bench:: bin/why3.@OCAMLBEST@ bin/why3config.@OCAMLBEST@ plugins $(TOOLS) \
# $(MAKE) test-api-mlw-tree.@OCAMLBEST@
# $(MAKE) test-api-mlw.@OCAMLBEST@
$(MAKE) test-session.@OCAMLBEST@
# $(MAKE) test-ocaml-extraction
$(MAKE) test-ocaml-extraction
# desactivé car requiert findlib
# if test -d examples/runstrat ; then \
# $(MAKE) test-runstrat.@OCAMLBEST@ ; fi
......
bench/bench
View file @ 6ee33b56
......@@ -198,6 +198,7 @@ goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/to_port
goods examples/foveoos11-cm
goods examples/WP_revisited
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
......@@ -233,13 +234,13 @@ execute examples/quicksort.mlw Test.bench
execute examples/conjugate.mlw Test.bench
# fails: needs support for "val" without code (how to do it?)
# examples/vacid_0_sparse_array.mlw Harness.bench
execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
# execute examples/knuth_prime_numbers.mlw PrimeNumbers.bench
execute examples/vstte10_max_sum.mlw TestCase.test_case
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixSort_test.bench
execute examples/verifythis_fm2012_LRS.mlw SuffixArray_test.bench
execute examples/verifythis_fm2012_LRS.mlw LRS_test.bench
execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
# execute examples/verifythis_PrefixSumRec.mlw PrefixSumRec.bench
execute examples/vstte10_queens.mlw NQueens.test8
# fails: "Cannot decide condition of if: (not ((~)((<<)((~)(0), 8)) = 0))"
# examples/queens.mlw NQueensBits.test8
......@@ -250,7 +251,7 @@ echo ""
echo "=== Checking extraction to OCaml ==="
extract_and_run examples/euler001 euler001.ml 1000000
extract_and_run examples/gcd gcd.ml 6 15
# extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
extract_and_run examples/defunctionalization defunctionalization.ml
......
examples/avl/avl/why3session.xml
View file @ 6ee33b56
......@@ -18,7 +18,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
</theory>
<theory name="AVL" sum="685a6c3f9ca1d8850254333db1860c27">
<theory name="AVL" sum="fbe4c9b252772ab5f1d75809246c2f5a">
<goal name="M.M.assoc">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
......@@ -259,7 +259,7 @@
<proof prover="0"><result status="valid" time="0.26" steps="667"/></proof>
</goal>
<goal name="VC insert.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.51" steps="1079"/></proof>
<proof prover="0"><result status="valid" time="0.36" steps="1079"/></proof>
</goal>
<goal name="VC insert.12" expl="12. variant decrease">
<proof prover="0"><result status="valid" time="0.08" steps="282"/></proof>
......
examples/avl/monoid.mlw
View file @ 6ee33b56
......@@ -46,14 +46,14 @@ module MonoidSumDef
let rec ghost function agg (f:'a -> t) (s:seq 'a) : M.t
variant { length s }
= if length s = 0 then zero else op (f s[0]) (agg f s[1 ..])
= if pure { length s = 0 } then {zero} else {op} (f s[0]) (agg f s[1 ..])
lemma agg_sing_core : forall s:seq 'a. length s = 1 -> s[1 ..] == empty
let rec lemma agg_cat (f:'a -> t) (s1 s2:seq 'a)
ensures { agg f (s1++s2) = op (agg f s1) (agg f s2) }
variant { length s1 }
= if length s1 <> 0 then let s3 = s1[1 ..] in agg_cat f s3 s2
= if pure { length s1 <> 0 } then let s3 = s1[1 ..] in agg_cat f s3 s2
clone MonoidSum as MS with type M.t = M.t,
constant M.zero = M.zero,
......
examples/avl/priority_queue.mlw
View file @ 6ee33b56
......@@ -216,7 +216,7 @@ module PQueue
use import seq.Occ
let ghost function to_bag (s:seq 'a) : 'a -> int =
fun x -> occ x s 0 (length s)
fun x -> pure { occ x s 0 (length s) }
let lemma to_bag_mem (x:'a) (s:seq 'a)
ensures { s.to_bag x > 0 <-> exists i. 0 <= i < length s /\ s[i] = x}
......@@ -278,7 +278,7 @@ module PQueue
ensures { forall d. 0 <= t.bag d <= t.card }
ensures { t.card >= 0 /\ (t.card > 0 -> t.bag t.minimum > 0) }
ensures { forall d. 0 < t.bag d -> CO.le t.minimum.key d.key }
= if t.m.card > 0
= if pure { t.m.card > 0 }
then let r0 = Sel.default_split () in
let _ = Sel.split r0 () t in
()
......
examples/avl/priority_queue/why3session.xml
View file @ 6ee33b56
......@@ -4,9 +4,10 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="1.8-001" timelimit="20" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../priority_queue.mlw">
<theory name="PQueue" sum="0ea25d1c19873a8bed56ba6c254a64ca">
<theory name="PQueue" sum="45f14173f723aa5e57e334d3cdecee7c">
<goal name="VC balancing" expl="VC for balancing">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
......@@ -34,28 +35,32 @@
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC assoc_m.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC assoc_m.9" expl="9. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC assoc_m.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC assoc_m.11" expl="11. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC assoc_m.12" expl="12. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC assoc_m.13" expl="13. postcondition">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC assoc_m.14" expl="14. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC assoc_m.15" expl="15. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<transf name="split_goal_wp">
<goal name="VC assoc_m.8.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC assoc_m.8.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC assoc_m.8.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC assoc_m.8.4" expl="4. postcondition">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC assoc_m.8.5" expl="5. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC assoc_m.8.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC assoc_m.8.7" expl="7. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC assoc_m.8.8" expl="8. postcondition">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
......@@ -113,10 +118,10 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC monoid_sum_is_min.5.2" expl="2. VC for monoid_sum_is_min">
<proof prover="1"><result status="valid" time="2.70"/></proof>
<proof prover="1"><result status="valid" time="3.43"/></proof>
</goal>
<goal name="VC monoid_sum_is_min.5.3" expl="3. VC for monoid_sum_is_min">
<proof prover="1"><result status="valid" time="1.21"/></proof>
<proof prover="1"><result status="valid" time="2.06"/></proof>
</goal>
</transf>
</goal>
......@@ -130,13 +135,13 @@
<goal name="VC selected_is_min.2" expl="2. assertion">
<transf name="split_goal_wp">
<goal name="VC selected_is_min.2.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.76" steps="1663"/></proof>
<proof prover="0"><result status="valid" time="1.03" steps="1663"/></proof>
</goal>
<goal name="VC selected_is_min.2.2" expl="2. assertion">
<proof prover="1"><result status="valid" time="2.70"/></proof>
<proof prover="1"><result status="valid" time="4.46"/></proof>
</goal>
<goal name="VC selected_is_min.2.3" expl="3. assertion">
<proof prover="1"><result status="valid" time="0.52"/></proof>
<proof prover="1"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="VC selected_is_min.2.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
......@@ -196,7 +201,7 @@
<goal name="VC selected_part.2" expl="2. postcondition">
<transf name="split_goal_wp">
<goal name="VC selected_part.2.1" expl="1. VC for selected_part">
<proof prover="0"><result status="valid" time="0.09" steps="251"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="251"/></proof>
</goal>
<goal name="VC selected_part.2.2" expl="2. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="30"/></proof>
......@@ -208,31 +213,31 @@
<proof prover="0"><result status="valid" time="0.06" steps="124"/></proof>
</goal>
<goal name="VC selected_part.2.5" expl="5. VC for selected_part">
<proof prover="0"><result status="valid" time="0.05" steps="97"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="97"/></proof>
</goal>
<goal name="VC selected_part.2.6" expl="6. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC selected_part.2.7" expl="7. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="55"/></proof>
<proof prover="0"><result status="valid" time="0.09" steps="55"/></proof>
</goal>
<goal name="VC selected_part.2.8" expl="8. VC for selected_part">
<proof prover="0"><result status="valid" time="0.07" steps="149"/></proof>
</goal>
<goal name="VC selected_part.2.9" expl="9. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC selected_part.2.10" expl="10. VC for selected_part">
<proof prover="0"><result status="valid" time="0.14" steps="362"/></proof>
<proof prover="0"><result status="valid" time="0.15" steps="362"/></proof>
</goal>
<goal name="VC selected_part.2.11" expl="11. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="37"/></proof>
<proof prover="0"><result status="valid" time="0.13" steps="37"/></proof>
</goal>
<goal name="VC selected_part.2.12" expl="12. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="18"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="VC selected_part.2.13" expl="13. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="32"/></proof>
<proof prover="0"><result status="valid" time="0.04" steps="32"/></proof>
</goal>
</transf>
</goal>
......@@ -275,93 +280,57 @@
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="VC selected_part.3.13" expl="13. VC for selected_part">
<proof prover="0"><result status="valid" time="0.32" steps="829"/></proof>
<proof prover="0"><result status="valid" time="0.50" steps="829"/></proof>
</goal>
</transf>
</goal>
<goal name="VC selected_part.4" expl="4. postcondition">
<transf name="split_goal_wp">
<goal name="VC selected_part.4.1" expl="1. VC for selected_part">
<proof prover="0"><result status="valid" time="0.09" steps="460"/></proof>
<proof prover="0"><result status="valid" time="0.29" steps="702"/></proof>
</goal>
<goal name="VC selected_part.4.2" expl="2. VC for selected_part">
<proof prover="0"><result status="valid" time="0.04" steps="37"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
<goal name="VC selected_part.4.3" expl="3. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC selected_part.4.4" expl="4. VC for selected_part">
<proof prover="0"><result status="valid" time="0.04" steps="178"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="181"/></proof>
</goal>
<goal name="VC selected_part.4.5" expl="5. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="37"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="37"/></proof>
</goal>
<goal name="VC selected_part.4.6" expl="6. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC selected_part.4.7" expl="7. VC for selected_part">
<proof prover="0"><result status="valid" time="0.05" steps="115"/></proof>
<proof prover="0"><result status="valid" time="0.18" steps="517"/></proof>
</goal>
<goal name="VC selected_part.4.8" expl="8. VC for selected_part">
<proof prover="0"><result status="valid" time="0.40" steps="865"/></proof>
<transf name="split_goal_wp">
<goal name="VC selected_part.4.8.1" expl="1. VC for selected_part">
<proof prover="0"><result status="valid" time="0.65" steps="865"/></proof>
</goal>
<goal name="VC selected_part.4.8.2" expl="2. VC for selected_part">
<proof prover="0"><result status="valid" time="0.22" steps="654"/></proof>
</goal>
</transf>
</goal>
<goal name="VC selected_part.4.9" expl="9. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="VC selected_part.4.10" expl="10. VC for selected_part">
<proof prover="0"><result status="valid" time="0.25" steps="462"/></proof>
<proof prover="0"><result status="valid" time="0.14" steps="472"/></proof>
</goal>
<goal name="VC selected_part.4.11" expl="11. VC for selected_part">
<proof prover="0"><result status="valid" time="0.10" steps="214"/></proof>
<proof prover="0"><result status="valid" time="0.35" steps="885"/></proof>
</goal>
<goal name="VC selected_part.4.12" expl="12. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC selected_part.4.13" expl="13. VC for selected_part">
<proof prover="0"><result status="valid" time="0.07" steps="277"/></proof>
</goal>
</transf>
</goal>
<goal name="VC selected_part.5" expl="5. postcondition">
<transf name="split_goal_wp">
<goal name="VC selected_part.5.1" expl="1. VC for selected_part">
<proof prover="0"><result status="valid" time="0.05" steps="128"/></proof>
</goal>
<goal name="VC selected_part.5.2" expl="2. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
<goal name="VC selected_part.5.3" expl="3. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="VC selected_part.5.4" expl="4. VC for selected_part">
<proof prover="0"><result status="valid" time="0.06" steps="183"/></proof>
</goal>
<goal name="VC selected_part.5.5" expl="5. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="37"/></proof>
</goal>
<goal name="VC selected_part.5.6" expl="6. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="VC selected_part.5.7" expl="7. VC for selected_part">
<proof prover="0"><result status="valid" time="0.09" steps="230"/></proof>
</goal>
<goal name="VC selected_part.5.8" expl="8. VC for selected_part">
<proof prover="0"><result status="valid" time="0.22" steps="654"/></proof>
</goal>
<goal name="VC selected_part.5.9" expl="9. VC for selected_part">
<proof prover="0"><result status="valid" time="0.03" steps="21"/></proof>
</goal>
<goal name="VC selected_part.5.10" expl="10. VC for selected_part">
<proof prover="0"><result status="valid" time="0.29" steps="525"/></proof>
</goal>
<goal name="VC selected_part.5.11" expl="11. VC for selected_part">
<proof prover="0"><result status="valid" time="0.13" steps="387"/></proof>
</goal>
<goal name="VC selected_part.5.12" expl="12. VC for selected_part">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="VC selected_part.5.13" expl="13. VC for selected_part">
<proof prover="0"><result status="valid" time="0.58" steps="1205"/></proof>
<proof prover="0"><result status="valid" time="1.00" steps="1370"/></proof>
</goal>
</transf>
</goal>
......@@ -414,7 +383,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="34"/></proof>
</goal>
<goal name="VC to_bag_mem.1.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.10" steps="234"/></proof>
<proof prover="0"><result status="valid" time="0.23" steps="234"/></proof>
</goal>
<goal name="VC to_bag_mem.1.4" expl="4. VC for to_bag_mem">
<proof prover="0"><result status="valid" time="0.38" steps="642"/></proof>
......@@ -441,7 +410,7 @@
<proof prover="0"><result status="valid" time="0.17" steps="206"/></proof>
</goal>
<goal name="VC get_minimum_index.5" expl="5. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.54" steps="691"/></proof>
<proof prover="0"><result status="valid" time="0.70" steps="691"/></proof>
</goal>
<goal name="VC get_minimum_index.6" expl="6. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="53"/></proof>
......@@ -453,13 +422,13 @@
<proof prover="0"><result status="valid" time="0.03" steps="15"/></proof>
</goal>
<goal name="VC get_minimum_index.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.59" steps="542"/></proof>
<proof prover="0"><result status="valid" time="0.97" steps="542"/></proof>
</goal>
<goal name="VC get_minimum_index.10" expl="10. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
<goal name="VC get_minimum_index.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="0.62" steps="1368"/></proof>
<proof prover="0"><result status="valid" time="1.27" steps="1368"/></proof>
</goal>
<goal name="VC get_minimum_index.12" expl="12. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="12"/></proof>
......@@ -493,13 +462,10 @@
<proof prover="0"><result status="valid" time="0.15" steps="140"/></proof>
</goal>
<goal name="VC split_gives_minimum.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.76" steps="1163"/></proof>
</goal>
<goal name="VC split_gives_minimum.6" expl="6. assertion">
<proof prover="1"><result status="valid" time="0.28"/></proof>
<proof prover="1"><result status="valid" time="1.12"/></proof>
</goal>
<goal name="VC split_gives_minimum.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="0.42" steps="816"/></proof>
<goal name="VC split_gives_minimum.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.63" steps="802"/></proof>
</goal>
</transf>
</goal>
......@@ -515,7 +481,7 @@
<proof prover="0"><result status="valid" time="0.04" steps="83"/></proof>
</goal>
<goal name="VC correction.4" expl="4. postcondition">
<proof prover="0" timelimit="20"><result status="valid" time="9.73" steps="3185"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="16.00" steps="3185"/></proof>
</goal>
<goal name="VC correction.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.05" steps="33"/></proof>
......@@ -546,10 +512,10 @@
<proof prover="0"><result status="valid" time="0.03" steps="60"/></proof>
</goal>
<goal name="VC remove_count.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="1.91"/></proof>
<proof prover="1"><result status="valid" time="3.80"/></proof>
</goal>
<goal name="VC remove_count.3" expl="3. postcondition">
<proof prover="1"><result status="valid" time="8.12"/></proof>
<proof prover="2"><result status="valid" time="10.24"/></proof>
</goal>
</transf>
</goal>
......@@ -618,10 +584,10 @@
<proof prover="0"><result status="valid" time="0.12" steps="75"/></proof>
</goal>
<goal name="VC pop_min.4.2" expl="2. VC for pop_min">
<proof prover="0" timelimit="5"><result status="valid" time="1.08" steps="613"/></proof>
<proof prover="0" timelimit="5"><result status="valid" time="1.08" steps="612"/></proof>
</goal>
<goal name="VC pop_min.4.3" expl="3. VC for pop_min">
<proof prover="0" timelimit="20"><result status="valid" time="6.53" steps="2308"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="7.64" steps="2306"/></proof>
</goal>
</transf>
</goal>
......@@ -633,7 +599,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="69"/></proof>
</goal>
<goal name="VC add.2" expl="2. postcondition">
<proof prover="0" timelimit="20"><result status="valid" time="7.95" steps="3519"/></proof>
<proof prover="0" timelimit="20"><result status="valid" time="7.95" steps="3221"/></proof>
</goal>
<goal name="VC add.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
......
examples/avl/ral/why3session.xml
View file @ 6ee33b56
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../ral.mlw">
<theory name="RAL" sum="8eef46a79b8f7e645bf03e91400b9f70">
<theory name="RAL" sum="23b1953119a07d783af66468a25d4402">
<goal name="VC balancing" expl="VC for balancing">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
......
examples/avl/tables.mlw
View file @ 6ee33b56
......@@ -135,7 +135,7 @@ module MapBase
requires { selection_possible () s /\ domain s k }
ensures { forall i. 0 <= i < length s /\ CO.eq s[i].key k -> result = s[i] }
= let j = ref 0 in
while not CO.eq s[!j].key k do
while not {CO.eq} s[!j].key k do
invariant { 0 <= !j < length s }
invariant { CO.le s[!j].key k }
variant { length s - !j }
......
examples/avl/tables/why3session.xml
View file @ 6ee33b56
This diff is collapsed.
examples/binary_search/why3session.xml
View file @ 6ee33b56
......@@ -14,7 +14,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="a953b8e11e9f21bbfb9646867928ce58" expanded="true">
<theory name="BinarySearchInt32" sum="1ae28c49a2dbfd082c313f20f784c903" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="3"><result status="valid" time="2.52" steps="3682"/></proof>
</goal>
......
examples/binary_search_vc_sp/why3session.xml
View file @ 6ee33b56
......@@ -97,7 +97,7 @@
</transf>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="f8439b7727009b247777048bf19a45ff" expanded="true">
<theory name="BinarySearchInt32" sum="0ffe15153f7e23ef8f6eea186bc06455" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="1. integer overflow">
......
examples/double_wp/compiler.mlw
View file @ 6ee33b56
......@@ -34,7 +34,7 @@ module Compile_aexpr
| Asub a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 -- $ isubf ()
| Amul a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 -- $ imulf ()
end in
hoare trivial_pre c (aexpr_post a c.wcode.length)
hoare {trivial_pre} c ({aexpr_post} a c.wcode.length)
(* Check that the above specification indeed implies the
natural one. *)
......@@ -83,7 +83,7 @@ module Compile_bexpr
| Bfalse -> $ if cond then inil () else ibranchf ofs
| Bnot b1 -> $ compile_bexpr b1 (not cond) ofs
| Band b1 b2 ->
let c2 = $ compile_bexpr b2 cond ofs % exec_cond b1 true in
let c2 = $ compile_bexpr b2 cond ofs % {exec_cond} b1 true in
let ofs = if cond then length c2.wcode else ofs + length c2.wcode in
$ compile_bexpr b1 false ofs -- c2
| Beq a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --
......@@ -91,8 +91,9 @@ module Compile_bexpr
| Ble a1 a2 -> $ compile_aexpr a1 -- $ compile_aexpr a2 --
$ if cond then iblef ofs else ibgtf ofs
end in
let ghost post = bexpr_post b cond (c.wcode.length + ofs) c.wcode.length in
hoare trivial_pre c post
let ghost post =
{bexpr_post} b cond (c.wcode.length + ofs) c.wcode.length in
hoare {trivial_pre} c post
(* Check that the above specification implies the natural one. *)
let compile_bexpr_natural (b:bexpr) (cond:bool) (ofs:ofs) : code
......@@ -146,11 +147,11 @@ module Compile_com
meta rewrite_def function loop_invariant
function loop_variant (c:com) (test:bexpr) : post 'a =
fun _ _ msj msi -> let VMS pj sj mj = msj in let VMS pi si mi = msi in
fun _ _ msj msi -> let VMS _pj _sj mj = msj in let VMS _pi _si mi = msi in
ceval mi c mj /\ beval mi test
lemma loop_variant_lemma : forall c test,x:'a,p msj msi.
loop_variant c test x p msj msi =
let VMS pj sj mj = msj in let VMS pi si mi = msi in
let VMS _pj _sj mj = msj in let VMS _pi _si mi = msi in
ceval mi c mj /\ beval mi test
meta rewrite lemma loop_variant_lemma
......@@ -174,20 +175,20 @@ module Compile_com
| Cif cond cmd1 cmd2 -> let code_false = compile_com cmd2 in
let code_true = $ compile_com cmd1 -- $ ibranchf code_false.code.length in
$ compile_bexpr cond false code_true.wcode.length --
(code_true % exec_cond cond true) --
($ code_false % exec_cond_old cond false)
(code_true % {exec_cond} cond true) --
($ code_false % {exec_cond_old} cond false)
| Cwhile test body ->
let code_body = compile_com body in
let body_length = length code_body.code + 1 in
let code_test = compile_bexpr test false body_length in
let ofs = length code_test.code + body_length in
let wp_while = $ code_test --
($ code_body -- $ ibranchf (- ofs)) % exec_cond test true in
let ghost inv = loop_invariant cmd in
let ghost var = loop_variant body test in
$ inil () -- make_loop wp_while inv (exec_cond test true) var
($ code_body -- $ ibranchf (- ofs)) % {exec_cond} test true in
let ghost inv = {loop_invariant} cmd in
let ghost var = {loop_variant} body test in
$ inil () -- make_loop wp_while inv ({exec_cond} test true) var
end in
hoare (com_pre cmd) res (com_post cmd res.wcode.length)
hoare ({com_pre} cmd) res ({com_post} cmd res.wcode.length)
(* Get back to natural specification for the compiler. *)
let compile_com_natural (com: com) : code
......
examples/double_wp/logic.mlw
View file @ 6ee33b56
......@@ -69,7 +69,7 @@ module Compiler_logic
ensures { result.wcode.length --> s1.wcode.length + s2.wcode.length }
ensures { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp }
= let code = s1.wcode ++ s2.wcode in
let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
let res = { wcode = code; wp = {seq_wp} s1.wcode.length s1.wp s2.wp } in
assert { forall x: 'a, p post ms. res.wp x p post ms ->
not (exists ms'. post ms' /\ contextual_irrelevance res.wcode p ms ms') ->
(forall ms'. s2.wp (x,ms) (p + s1.wcode.length) post ms' /\
......@@ -91,7 +91,7 @@ module Compiler_logic
let (%) (s:wp 'a) (ghost cond:pre {'a}) : wp 'a
ensures { result.wp --> fork_wp s.wp cond }
ensures { result.wcode.length --> s.wcode.length }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
= { wcode = s.wcode; wp = {fork_wp} s.wp cond }
(* WP transformer for hoare triples. *)
function towp_wp (pr:pre 'a) (ps:post 'a) : wp_trans 'a =
......@@ -107,7 +107,7 @@ module Compiler_logic
let ($_) (c:hl 'a) : wp 'a
ensures { result.wcode.length --> c.code.length }
ensures { result.wp --> towp_wp c.pre c.post }
= { wcode = c.code; wp = towp_wp c.pre c.post }
= { wcode = c.code; wp = {towp_wp} c.pre c.post }
(* Equip code with pre/post-condition. That is here that proof happen.
(P -> wp (c,Q)). Anologous to checking function/abstract block
......@@ -156,7 +156,7 @@ module Compiler_logic
(ghost var:post {'a}) : wp 'a
ensures { result.wp --> loop_wp c.wp inv cont var }
ensures { result.wcode.length --> c.wcode.length }
= let wpt = loop_wp c.wp inv cont var in
= let wpt = pure { loop_wp c.wp inv cont var } in
assert { forall x p q ms0. wpt x p q ms0 ->
forall ms. inv x p ms -> acc (var x p) ms ->