Commit 265a349f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

remove legitimate warning by turning axiom Bertrand into an unproved lemma

parent 832328e5
......@@ -17,7 +17,7 @@
Truly a tour de force, this proof includes the full proof of Bertrand's
postulate in Coq. Here, we simply focus on the program verification part,
assuming Bertrand's postulate as an axiom.
posing Bertrand's postulate as a lemma that we do not prove.
Note: Knuth's code is entering the loop where a new prime number is
added, thus resulting into the immediate addition of 3 as prime[1].
......@@ -55,7 +55,7 @@ module PrimeNumbers
forall d: int. 2 <= d <= p[u-1] -> prime d ->
exists i: int. 0 <= i < u /\ d = p[i]
axiom Bertrand_postulate:
lemma Bertrand_postulate:
forall p: int. prime p -> not (no_prime_in p (2*p))
(* returns an array containing the first m prime numbers *)
......
......@@ -4,69 +4,71 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl4" timelimit="5" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="4000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="5" memlimit="4000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="Z3" version="2.19" timelimit="10" memlimit="0"/>
<prover id="5" name="CVC3" version="2.2" timelimit="10" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../knuth_prime_numbers.mlw" expanded="true">
<theory name="PrimeNumbers" sum="3a516751476c7d18c8997f24cdb57dd2" expanded="true">
<theory name="PrimeNumbers" sum="7b0b6d08289ea7110d80282929da3550" expanded="true">
<goal name="exists_prime">
<proof prover="1" timelimit="10" memlimit="0" edited="knuth_prime_numbers_WP_PrimeNumbers_exists_prime_1.v"><result status="valid" time="1.41"/></proof>
</goal>
<goal name="Bertrand_postulate" expanded="true">
</goal>
<goal name="WP_parameter prime_numbers" expl="VC for prime_numbers">
<transf name="split_goal_wp">
<goal name="WP_parameter prime_numbers.1" expl="1. array creation size">
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.2" expl="2. index in array bounds">
<proof prover="2" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.3" expl="3. index in array bounds">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.4" expl="4. postcondition">
<proof prover="2" memlimit="0"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3" memlimit="0"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.5" expl="5. loop invariant init">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.6" expl="6. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.7" expl="7. loop invariant init">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.8" expl="8. loop invariant init">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.9" expl="9. index in array bounds">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.10" expl="10. assertion">
<proof prover="1" edited="knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_5.v"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.11" expl="11. variant decrease">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.12" expl="12. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.13" expl="13. precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.14" expl="14. precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter prime_numbers.14.1" expl="1.">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.14.2" expl="2.">
<proof prover="1" edited="knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_6.v"><result status="valid" time="1.68"/></proof>
......@@ -74,30 +76,30 @@
</transf>
</goal>
<goal name="WP_parameter prime_numbers.15" expl="15. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.16" expl="16. precondition">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.17" expl="17. precondition">
<proof prover="2" timelimit="5"><result status="valid" time="0.06"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.18" expl="18. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.19" expl="19. index in array bounds">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.20" expl="20. index in array bounds">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.21" expl="21. variant decrease">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.22" expl="22. precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter prime_numbers.22.1" expl="1.">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.22.2" expl="2.">
<proof prover="1" edited="knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_7.v"><result status="valid" time="1.73"/></proof>
......@@ -105,52 +107,52 @@
</transf>
</goal>
<goal name="WP_parameter prime_numbers.23" expl="23. precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.24" expl="24. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.25" expl="25. precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.26" expl="26. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.27" expl="27. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.28" expl="28. postcondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.29" expl="29. assertion">
<proof prover="1" edited="knuth_prime_numbers_WP_PrimeNumbers_WP_parameter_prime_numbers_4.v"><result status="valid" time="3.35"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.30" expl="30. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.31" expl="31. type invariant">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.32" expl="32. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.33" expl="33. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.34" expl="34. precondition">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.35" expl="35. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.36" expl="36. precondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.37" expl="37. precondition">
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.38" expl="38. index in array bounds">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.39" expl="39. loop invariant preservation">
<transf name="inline_goal">
......@@ -158,7 +160,7 @@
<transf name="split_goal_wp">
<goal name="WP_parameter prime_numbers.39.1.1" expl="1.">
<proof prover="0"><result status="valid" time="0.97"/></proof>
<proof prover="3" memlimit="1000"><result status="valid" time="0.09"/></proof>
<proof prover="2" memlimit="1000"><result status="valid" time="0.09"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -168,8 +170,7 @@
</goal>
<goal name="WP_parameter prime_numbers.39.1.3" expl="3.">
<proof prover="5"><result status="valid" time="0.11"/></proof>
<metas
expanded="true">
<metas>
<ts_pos name="ref" arity="1" id="2761"
ip_theory="Ref">
<ip_library name="ref"/>
......@@ -290,22 +291,22 @@
<ip_library name="map"/>
<ip_qualid name="const"/>
</ls_pos>
<ls_pos name="set" id="3572"
<ls_pos name="set" id="3362"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3614"
<ls_pos name="mixfix [&lt;-]" id="3404"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="make" id="3715"
<ls_pos name="make" id="3505"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="make"/>
</ls_pos>
<ls_pos name="first_primes" id="6143"
<ls_pos name="first_primes" id="6033"
ip_theory="PrimeNumbers">
<ip_qualid name="first_primes"/>
</ls_pos>
......@@ -783,11 +784,11 @@
<ip_library name="map"/>
<ip_qualid name="Const"/>
</pr_pos>
<pr_pos name="exists_prime" id="6170"
<pr_pos name="exists_prime" id="6060"
ip_theory="PrimeNumbers">
<ip_qualid name="exists_prime"/>
</pr_pos>
<pr_pos name="Bertrand_postulate" id="6183"
<pr_pos name="Bertrand_postulate" id="6073"
ip_theory="PrimeNumbers">
<ip_qualid name="Bertrand_postulate"/>
</pr_pos>
......@@ -861,16 +862,16 @@
<meta_arg_ls id="2967"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3572"/>
<meta_arg_ls id="3362"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3614"/>
<meta_arg_ls id="3404"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3715"/>
<meta_arg_ls id="3505"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="6143"/>
<meta_arg_ls id="6033"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1557"/>
......@@ -1152,20 +1153,20 @@
<meta_arg_pr id="2969"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="6170"/>
<meta_arg_pr id="6060"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="6183"/>
<meta_arg_pr id="6073"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2761"/>
</meta>
<goal name="WP_parameter prime_numbers.39.1.3" expl="3." expanded="true">
<transf name="eliminate_builtin" expanded="true">
<goal name="WP_parameter prime_numbers.39.1.3.1" expl="1." expanded="true">
<goal name="WP_parameter prime_numbers.39.1.3" expl="3.">
<transf name="eliminate_builtin">
<goal name="WP_parameter prime_numbers.39.1.3.1" expl="1.">
<proof prover="0" timelimit="10"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="3" timelimit="10" memlimit="1000"><result status="valid" time="0.80"/></proof>
<proof prover="2" timelimit="10" memlimit="1000"><result status="valid" time="0.80"/></proof>
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
......@@ -1174,8 +1175,7 @@
</goal>
<goal name="WP_parameter prime_numbers.39.1.4" expl="4.">
<proof prover="5"><result status="valid" time="0.12"/></proof>
<metas
expanded="true">
<metas>
<ts_pos name="ref" arity="1" id="2761"
ip_theory="Ref">
<ip_library name="ref"/>
......@@ -1296,22 +1296,22 @@
<ip_library name="map"/>
<ip_qualid name="const"/>
</ls_pos>
<ls_pos name="set" id="3572"
<ls_pos name="set" id="3362"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="set"/>
</ls_pos>
<ls_pos name="mixfix [&lt;-]" id="3614"
<ls_pos name="mixfix [&lt;-]" id="3404"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="mixfix [&lt;-]"/>
</ls_pos>
<ls_pos name="make" id="3715"
<ls_pos name="make" id="3505"
ip_theory="Array">
<ip_library name="array"/>
<ip_qualid name="make"/>
</ls_pos>
<ls_pos name="first_primes" id="6143"
<ls_pos name="first_primes" id="6033"
ip_theory="PrimeNumbers">
<ip_qualid name="first_primes"/>
</ls_pos>
......@@ -1789,11 +1789,11 @@
<ip_library name="map"/>
<ip_qualid name="Const"/>
</pr_pos>
<pr_pos name="exists_prime" id="6170"
<pr_pos name="exists_prime" id="6060"
ip_theory="PrimeNumbers">
<ip_qualid name="exists_prime"/>
</pr_pos>
<pr_pos name="Bertrand_postulate" id="6183"
<pr_pos name="Bertrand_postulate" id="6073"
ip_theory="PrimeNumbers">
<ip_qualid name="Bertrand_postulate"/>
</pr_pos>
......@@ -1867,16 +1867,16 @@
<meta_arg_ls id="2967"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3572"/>
<meta_arg_ls id="3362"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3614"/>
<meta_arg_ls id="3404"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="3715"/>
<meta_arg_ls id="3505"/>
</meta>
<meta name="remove_logic">
<meta_arg_ls id="6143"/>
<meta_arg_ls id="6033"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="1557"/>
......@@ -2158,19 +2158,19 @@
<meta_arg_pr id="2969"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="6170"/>
<meta_arg_pr id="6060"/>
</meta>
<meta name="remove_prop">
<meta_arg_pr id="6183"/>
<meta_arg_pr id="6073"/>
</meta>
<meta name="remove_type">
<meta_arg_ts id="2761"/>
</meta>
<goal name="WP_parameter prime_numbers.39.1.4" expl="4." expanded="true">
<transf name="eliminate_builtin" expanded="true">
<goal name="WP_parameter prime_numbers.39.1.4.1" expl="1." expanded="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3" timelimit="10" memlimit="1000"><result status="valid" time="2.54"/></proof>
<goal name="WP_parameter prime_numbers.39.1.4" expl="4.">
<transf name="eliminate_builtin">
<goal name="WP_parameter prime_numbers.39.1.4.1" expl="1.">
<proof prover="2" timelimit="10" memlimit="1000"><result status="valid" time="2.54"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
......@@ -2182,19 +2182,19 @@
</transf>
</goal>
<goal name="WP_parameter prime_numbers.40" expl="40. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.41" expl="41. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.42" expl="42. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.26"/></proof>
<proof prover="2"><result status="valid" time="0.26"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.43" expl="43. type invariant">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.44" expl="44. postcondition">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
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