Commit 077ae9c6 authored by MARCHE Claude's avatar MARCHE Claude

Merge remote-tracking branch 'origin/master' into new_system

Conflicts:
	examples/fibonacci.mlw
	examples/fibonacci/why3session.xml
	examples/fibonacci/why3shapes.gz
	examples/koda_ruskey/why3session.xml
	examples/koda_ruskey/why3shapes.gz
	examples/schorr_waite_via_recursion/why3session.xml
	examples/schorr_waite_via_recursion/why3shapes.gz
	examples/tests-provers/bv/why3session.xml
	examples/tests-provers/bv/why3shapes.gz
	examples/tests-provers/ieee_float/why3session.xml
	examples/tree_of_array/why3session.xml
	examples/tree_of_array/why3shapes.gz
	examples/vstte12_bfs/why3session.xml
	examples/vstte12_bfs/why3shapes.gz
	theories/int.why
	theories/real.why
parents be829554 3e625c03
...@@ -101,7 +101,7 @@ ...@@ -101,7 +101,7 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="IntArrayCursor" sum="8090cb9a5eb720659015e09ae27d5ddf" expanded="true"> <theory name="IntArrayCursor" sum="0e0d1427d3bf976c46e43f3795d29aa6" expanded="true">
<goal name="WP_parameter create" expl="VC for create" expanded="true"> <goal name="WP_parameter create" expl="VC for create" expanded="true">
<proof prover="5"><result status="valid" time="0.05" steps="15"/></proof> <proof prover="5"><result status="valid" time="0.05" steps="15"/></proof>
</goal> </goal>
...@@ -137,12 +137,12 @@ ...@@ -137,12 +137,12 @@
<proof prover="1"><result status="unknown" time="0.05"/></proof> <proof prover="1"><result status="unknown" time="0.05"/></proof>
</goal> </goal>
<goal name="WP_parameter next.4" expl="4. postcondition"> <goal name="WP_parameter next.4" expl="4. postcondition">
<proof prover="2"><result status="valid" time="0.27"/></proof> <proof prover="2"><result status="valid" time="0.41"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="TestArrayCursor" sum="32c64c0426c4c4a9eb75e763071b02bd"> <theory name="TestArrayCursor" sum="7d18da58ded19d7039316e45244f1693">
<goal name="WP_parameter array_sum_array_to_list" expl="VC for array_sum_array_to_list"> <goal name="WP_parameter array_sum_array_to_list" expl="VC for array_sum_array_to_list">
<proof prover="1"><result status="valid" time="0.04" steps="46"/></proof> <proof prover="1"><result status="valid" time="0.04" steps="46"/></proof>
</goal> </goal>
......
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="9" name="Alt-Ergo" version="1.00.prv" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../dijkstra.mlw" expanded="true"> <file name="../dijkstra.mlw" expanded="true">
<theory name="DijkstraShortestPath" sum="927fe939ad868be15f33edef384e9149" expanded="true"> <theory name="DijkstraShortestPath" sum="56fdafe8906f0c9270722a213f328c54" expanded="true">
<goal name="WP_parameter relax" expl="VC for relax"> <goal name="WP_parameter relax" expl="VC for relax">
<transf name="split_goal_wp"> <transf name="split_goal_wp">
<goal name="WP_parameter relax.1" expl="1. postcondition"> <goal name="WP_parameter relax.1" expl="1. postcondition">
...@@ -134,7 +134,7 @@ ...@@ -134,7 +134,7 @@
<proof prover="8"><result status="valid" time="0.04" steps="86"/></proof> <proof prover="8"><result status="valid" time="0.04" steps="86"/></proof>
</goal> </goal>
<goal name="WP_parameter shortest_path_code.12.1.2" expl="2. VC for shortest_path_code"> <goal name="WP_parameter shortest_path_code.12.1.2" expl="2. VC for shortest_path_code">
<proof prover="2" timelimit="10"><result status="valid" time="0.84"/></proof> <proof prover="2" timelimit="10"><result status="valid" time="1.08"/></proof>
</goal> </goal>
<goal name="WP_parameter shortest_path_code.12.1.3" expl="3. VC for shortest_path_code"> <goal name="WP_parameter shortest_path_code.12.1.3" expl="3. VC for shortest_path_code">
<proof prover="8"><result status="valid" time="0.03" steps="25"/></proof> <proof prover="8"><result status="valid" time="0.03" steps="25"/></proof>
......
...@@ -7,7 +7,7 @@ ...@@ -7,7 +7,7 @@
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.3" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.3" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../logic.mlw"> <file name="../logic.mlw">
<theory name="Compiler_logic" sum="01e7845ed8490da8741a9ca86ba106c9"> <theory name="Compiler_logic" sum="c12240d535cc2c746aa01470b9422232">
<goal name="seq_wp_lemma"> <goal name="seq_wp_lemma">
<proof prover="2"><result status="valid" time="0.04" steps="8"/></proof> <proof prover="2"><result status="valid" time="0.04" steps="8"/></proof>
</goal> </goal>
...@@ -72,7 +72,7 @@ ...@@ -72,7 +72,7 @@
</goal> </goal>
<goal name="WP_parameter make_loop_hl.1.2" expl="2. assertion"> <goal name="WP_parameter make_loop_hl.1.2" expl="2. assertion">
<transf name="induction_pr"> <transf name="induction_pr">
<goal name="WP_parameter make_loop_hl.1.2.1" expl="1. VC for make_loop_hl"> <goal name="WP_parameter make_loop_hl.1.2.1" expl="1. assertion">
<transf name="simplify_trivial_quantification_in_goal"> <transf name="simplify_trivial_quantification_in_goal">
<goal name="WP_parameter make_loop_hl.1.2.1.1" expl="1. VC for make_loop_hl"> <goal name="WP_parameter make_loop_hl.1.2.1.1" expl="1. VC for make_loop_hl">
<transf name="compute_specified"> <transf name="compute_specified">
......
...@@ -3,19 +3,20 @@ ...@@ -3,19 +3,20 @@
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4"> <why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="0" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vm.mlw" expanded="true"> <file name="../vm.mlw" expanded="true">
<theory name="ReflTransClosure" sum="b95bd9cec6f5b6d4f89525010d16d760"> <theory name="ReflTransClosure" sum="f262a809b2b34d0ef483b05c11f8827b">
<goal name="transition_star_one"> <goal name="transition_star_one">
<proof prover="0"><result status="valid" time="0.00"/></proof> <proof prover="0"><result status="valid" time="0.00"/></proof>
</goal> </goal>
<goal name="transition_star_transitive"> <goal name="transition_star_transitive">
<transf name="induction_pr"> <transf name="induction_pr">
<goal name="transition_star_transitive.1" expl="1."> <goal name="transition_star_transitive.1" expl="1.">
<proof prover="2"><result status="valid" time="0.01" steps="4"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal> </goal>
<goal name="transition_star_transitive.2" expl="2."> <goal name="transition_star_transitive.2" expl="2.">
<proof prover="0"><result status="valid" time="0.01"/></proof> <proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
...@@ -271,13 +271,10 @@ theory Mat22 "2x2 integer matrices" ...@@ -271,13 +271,10 @@ theory Mat22 "2x2 integer matrices"
a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22; a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22;
} }
(* holds, but not useful *)
(* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *)
clone export clone export
int.Exponentiation with int.Exponentiation with
type t = t, function one = id, function (*) = mult, type t = t, function one = id, function (*) = mult,
goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r goal Assoc, goal Unit_def_l, goal Unit_def_r
end end
......
...@@ -245,7 +245,7 @@ theory Exponentiation ...@@ -245,7 +245,7 @@ theory Exponentiation
constant one : t constant one : t
function (*) t t : t function (*) t t : t
clone export algebra.CommutativeMonoid clone export algebra.Monoid
with type t = t, constant unit = one, function op = (*) with type t = t, constant unit = one, function op = (*)
(* TODO: implement with let rec once let cloning is done *) (* TODO: implement with let rec once let cloning is done *)
...@@ -293,7 +293,7 @@ theory Power ...@@ -293,7 +293,7 @@ theory Power
clone export Exponentiation with clone export Exponentiation with
type t = int, constant one = one, type t = int, constant one = one,
function (*) = (*), function power = power, function (*) = (*), function power = power,
goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r goal Assoc, goal Unit_def_l, goal Unit_def_r
lemma Power_non_neg: lemma Power_non_neg:
forall x y. x >= 0 /\ y >= 0 -> power x y >= 0 forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
......
...@@ -255,7 +255,7 @@ theory PowerInt ...@@ -255,7 +255,7 @@ theory PowerInt
clone export int.Exponentiation with clone export int.Exponentiation with
type t = real, constant one = Real.one, function (*) = Real.(*), type t = real, constant one = Real.one, function (*) = Real.(*),
goal Assoc, goal Comm, goal Unit_def_l, goal Unit_def_r goal Assoc, goal Unit_def_l, goal Unit_def_r
lemma Pow_ge_one: lemma Pow_ge_one:
forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n forall x:real, n:int. 0 <= n /\ 1.0 <=. x -> 1.0 <=. power x n
......
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