Commit 2d8a7f6b authored by MARCHE Claude's avatar MARCHE Claude

updated sessions after fixing the name of subgoals

parent 7b4c606e
......@@ -127,19 +127,19 @@ scheduled on Oct 2012
== New Features to announce ==
Programs:
o new API for programs
o new concrete syntax for programs
o new API for programs
o type invariants
o ghost code
Transformations:
o transformations for induction
o induction (experimental, undocumented)
o bisection (experimental, undocumented)
Provers support:
o Support for Coq 8.4
o support for Coq 8.4
o dropped support for Coq 8.2
o new scheme for Coq realizations using type classes
o Support for PVS 6.0, including realizations
o support for forthcoming PVS 6.0, including realizations
o support for iProver and Zenon
Misc:
......@@ -154,6 +154,7 @@ Misc:
instead
Bug fixes:
o Coq output uses type classes to ensure Why3 types are inhabited
o fixed bug on merging config files which prevented the use
of Why3 back-end of the Frama-C/Jessie plugin when Coq is
not installed. (Bug 14672 of the Bug Tracking System)
......
......@@ -594,7 +594,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.75"/>
<result status="valid" time="2.27"/>
</proof>
</goal>
<goal
......
......@@ -286,7 +286,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter move_value_alpha_beta.1"
name="WP_parameter move_value_alpha_beta.2.1"
locfile="../alphaBeta.mlw"
loclnum="109" loccnumb="10" loccnume="31"
expl="1. postcondition"
......@@ -306,7 +306,7 @@
</proof>
</goal>
<goal
name="WP_parameter move_value_alpha_beta.2"
name="WP_parameter move_value_alpha_beta.2.2"
locfile="../alphaBeta.mlw"
loclnum="109" loccnumb="10" loccnume="31"
expl="2. postcondition"
......@@ -326,7 +326,7 @@
</proof>
</goal>
<goal
name="WP_parameter move_value_alpha_beta.3"
name="WP_parameter move_value_alpha_beta.2.3"
locfile="../alphaBeta.mlw"
loclnum="109" loccnumb="10" loccnume="31"
expl="3. postcondition"
......@@ -388,7 +388,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter negabeta.1"
name="WP_parameter negabeta.1.1"
locfile="../alphaBeta.mlw"
loclnum="121" loccnumb="7" loccnume="15"
expl="1. postcondition"
......@@ -416,7 +416,7 @@
</proof>
</goal>
<goal
name="WP_parameter negabeta.2"
name="WP_parameter negabeta.1.2"
locfile="../alphaBeta.mlw"
loclnum="121" loccnumb="7" loccnume="15"
expl="2. postcondition"
......@@ -444,7 +444,7 @@
</proof>
</goal>
<goal
name="WP_parameter negabeta.3"
name="WP_parameter negabeta.1.3"
locfile="../alphaBeta.mlw"
loclnum="121" loccnumb="7" loccnume="15"
expl="3. postcondition"
......@@ -489,7 +489,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter negabeta.1"
name="WP_parameter negabeta.2.1"
locfile="../alphaBeta.mlw"
loclnum="121" loccnumb="7" loccnume="15"
expl="1. postcondition"
......@@ -525,7 +525,7 @@
</proof>
</goal>
<goal
name="WP_parameter negabeta.2"
name="WP_parameter negabeta.2.2"
locfile="../alphaBeta.mlw"
loclnum="121" loccnumb="7" loccnume="15"
expl="2. postcondition"
......@@ -561,7 +561,7 @@
</proof>
</goal>
<goal
name="WP_parameter negabeta.3"
name="WP_parameter negabeta.2.3"
locfile="../alphaBeta.mlw"
loclnum="121" loccnumb="7" loccnume="15"
expl="3. postcondition"
......
......@@ -1199,7 +1199,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter counting_sort.1"
name="WP_parameter counting_sort.55.1"
locfile="../counting_sort.mlw"
loclnum="65" loccnumb="6" loccnume="19"
expl="1. loop invariant preservation"
......@@ -1244,7 +1244,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter counting_sort.1"
name="WP_parameter counting_sort.56.1"
locfile="../counting_sort.mlw"
loclnum="65" loccnumb="6" loccnume="19"
expl="1. loop invariant preservation"
......@@ -2577,7 +2577,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter in_place_counting_sort.1"
name="WP_parameter in_place_counting_sort.55.1"
locfile="../counting_sort.mlw"
loclnum="102" loccnumb="6" loccnume="28"
expl="1. loop invariant preservation"
......@@ -2622,7 +2622,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter in_place_counting_sort.1"
name="WP_parameter in_place_counting_sort.56.1"
locfile="../counting_sort.mlw"
loclnum="102" loccnumb="6" loccnume="28"
expl="1. loop invariant preservation"
......
......@@ -530,7 +530,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter distance.1"
name="WP_parameter distance.23.1"
locfile="../distance.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="1. assertion"
......@@ -545,7 +545,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter distance.1"
name="WP_parameter distance.23.1.1"
locfile="../distance.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="1. assertion"
......@@ -565,7 +565,7 @@
</proof>
</goal>
<goal
name="WP_parameter distance.2"
name="WP_parameter distance.23.1.2"
locfile="../distance.mlw"
loclnum="46" loccnumb="6" loccnume="14"
expl="2. assertion"
......
......@@ -1003,7 +1003,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter distance.1"
name="WP_parameter distance.37.1"
locfile="../edit_distance.mlw"
loclnum="139" loccnumb="6" loccnume="14"
expl="1. loop invariant preservation"
......
......@@ -146,7 +146,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter find.1"
name="WP_parameter find.5.1"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="1."
......@@ -166,7 +166,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.2"
name="WP_parameter find.5.2"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="2."
......@@ -219,7 +219,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter find.1"
name="WP_parameter find.6.1"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="1."
......@@ -247,7 +247,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.2"
name="WP_parameter find.6.2"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="2."
......@@ -267,7 +267,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.3"
name="WP_parameter find.6.3"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="3."
......@@ -287,7 +287,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.4"
name="WP_parameter find.6.4"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="4."
......@@ -384,7 +384,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter find.1"
name="WP_parameter find.10.1"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="1."
......@@ -404,7 +404,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.2"
name="WP_parameter find.10.2"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="2."
......@@ -424,7 +424,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.3"
name="WP_parameter find.10.3"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="3."
......@@ -444,7 +444,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.4"
name="WP_parameter find.10.4"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="4."
......@@ -802,7 +802,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter find.1"
name="WP_parameter find.27.1"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="1."
......@@ -822,7 +822,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.2"
name="WP_parameter find.27.2"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="2."
......@@ -842,7 +842,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.3"
name="WP_parameter find.27.3"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="3."
......@@ -862,7 +862,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.4"
name="WP_parameter find.27.4"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="4."
......@@ -882,7 +882,7 @@
</proof>
</goal>
<goal
name="WP_parameter find.5"
name="WP_parameter find.27.5"
locfile="../find.mlw"
loclnum="40" loccnumb="6" loccnume="10"
expl="5."
......
......@@ -878,7 +878,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter two_equal_elements.1"
name="WP_parameter two_equal_elements.42.1"
locfile="../foveoos11_challenge3.mlw"
loclnum="17" loccnumb="6" loccnume="24"
expl="1."
......@@ -898,7 +898,7 @@
</proof>
</goal>
<goal
name="WP_parameter two_equal_elements.2"
name="WP_parameter two_equal_elements.42.2"
locfile="../foveoos11_challenge3.mlw"
loclnum="17" loccnumb="6" loccnume="24"
expl="2."
......@@ -918,7 +918,7 @@
</proof>
</goal>
<goal
name="WP_parameter two_equal_elements.3"
name="WP_parameter two_equal_elements.42.3"
locfile="../foveoos11_challenge3.mlw"
loclnum="17" loccnumb="6" loccnume="24"
expl="3."
......
......@@ -312,7 +312,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter combine.1"
name="WP_parameter combine.8.1"
locfile="../generate_all_trees.mlw"
loclnum="46" loccnumb="6" loccnume="13"
expl="1. postcondition"
......@@ -349,7 +349,7 @@
</proof>
</goal>
<goal
name="WP_parameter combine.2"
name="WP_parameter combine.8.2"
locfile="../generate_all_trees.mlw"
loclnum="46" loccnumb="6" loccnume="13"
expl="2. postcondition"
......@@ -466,7 +466,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter combine.1"
name="WP_parameter combine.13.1"
locfile="../generate_all_trees.mlw"
loclnum="46" loccnumb="6" loccnume="13"
expl="1. postcondition"
......@@ -486,7 +486,7 @@
</proof>
</goal>
<goal
name="WP_parameter combine.2"
name="WP_parameter combine.13.2"
locfile="../generate_all_trees.mlw"
loclnum="46" loccnumb="6" loccnume="13"
expl="2. postcondition"
......@@ -563,7 +563,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter combine.1"
name="WP_parameter combine.16.1"
locfile="../generate_all_trees.mlw"
loclnum="46" loccnumb="6" loccnume="13"
expl="1. postcondition"
......@@ -583,7 +583,7 @@
</proof>
</goal>
<goal
name="WP_parameter combine.2"
name="WP_parameter combine.16.2"
locfile="../generate_all_trees.mlw"
loclnum="46" loccnumb="6" loccnume="13"
expl="2. postcondition"
......@@ -957,7 +957,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter all_trees.1"
name="WP_parameter all_trees.17.1"
locfile="../generate_all_trees.mlw"
loclnum="74" loccnumb="6" loccnume="15"
expl="1. loop invariant preservation"
......@@ -985,7 +985,7 @@
</proof>
</goal>
<goal
name="WP_parameter all_trees.2"
name="WP_parameter all_trees.17.2"
locfile="../generate_all_trees.mlw"
loclnum="74" loccnumb="6" loccnume="15"
expl="2. loop invariant preservation"
......
......@@ -599,7 +599,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.37"/>
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal
......
......@@ -233,7 +233,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter sqrt.1"
name="WP_parameter sqrt.3.1"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="1."
......@@ -277,7 +277,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.2"
name="WP_parameter sqrt.3.2"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="2."
......@@ -321,7 +321,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.3"
name="WP_parameter sqrt.3.3"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="3."
......@@ -349,7 +349,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.4"
name="WP_parameter sqrt.3.4"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="4."
......@@ -393,7 +393,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.5"
name="WP_parameter sqrt.3.5"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="5."
......@@ -454,7 +454,7 @@
proved="false"
expanded="true">
<goal
name="WP_parameter sqrt.1"
name="WP_parameter sqrt.4.1"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="1."
......@@ -498,7 +498,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.2"
name="WP_parameter sqrt.4.2"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="2."
......@@ -542,7 +542,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.3"
name="WP_parameter sqrt.4.3"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="3."
......@@ -586,7 +586,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.4"
name="WP_parameter sqrt.4.4"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="4."
......@@ -622,7 +622,7 @@
</proof>
</goal>
<goal
name="WP_parameter sqrt.5"
name="WP_parameter sqrt.4.5"
locfile="../isqrt.mlw"
loclnum="37" loccnumb="6" loccnume="10"
expl="5."
......
......@@ -490,7 +490,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter initnext.1"
name="WP_parameter initnext.13.1"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="1. loop invariant preservation"
......@@ -505,7 +505,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter initnext.1"
name="WP_parameter initnext.13.1.1"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="1. loop invariant preservation"
......@@ -525,7 +525,7 @@
</proof>
</goal>
<goal
name="WP_parameter initnext.2"
name="WP_parameter initnext.13.1.2"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="2. loop invariant preservation"
......@@ -545,7 +545,7 @@
</proof>
</goal>
<goal
name="WP_parameter initnext.3"
name="WP_parameter initnext.13.1.3"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="3. loop invariant preservation"
......@@ -565,7 +565,7 @@
</proof>
</goal>
<goal
name="WP_parameter initnext.4"
name="WP_parameter initnext.13.1.4"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="4. loop invariant preservation"
......@@ -705,7 +705,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter initnext.1"
name="WP_parameter initnext.19.1"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="1. loop invariant preservation"
......@@ -720,7 +720,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter initnext.1"
name="WP_parameter initnext.19.1.1"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="1. loop invariant preservation"
......@@ -740,7 +740,7 @@
</proof>
</goal>
<goal
name="WP_parameter initnext.2"
name="WP_parameter initnext.19.1.2"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="2. loop invariant preservation"
......@@ -760,7 +760,7 @@
</proof>
</goal>
<goal
name="WP_parameter initnext.3"
name="WP_parameter initnext.19.1.3"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="3. loop invariant preservation"
......@@ -780,7 +780,7 @@
</proof>
</goal>
<goal
name="WP_parameter initnext.4"
name="WP_parameter initnext.19.1.4"
locfile="../kmp.mlw"
loclnum="90" loccnumb="6" loccnume="14"
expl="4. loop invariant preservation"
......
......@@ -393,7 +393,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter prime_numbers.1"
name="WP_parameter prime_numbers.14.1"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="1."
......@@ -413,7 +413,7 @@
</proof>
</goal>
<goal
name="WP_parameter prime_numbers.2"
name="WP_parameter prime_numbers.14.2"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="2."
......@@ -599,7 +599,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter prime_numbers.1"
name="WP_parameter prime_numbers.22.1"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="1."
......@@ -619,7 +619,7 @@
</proof>
</goal>
<goal
name="WP_parameter prime_numbers.2"
name="WP_parameter prime_numbers.22.2"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="2."
......@@ -966,7 +966,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter prime_numbers.1"
name="WP_parameter prime_numbers.38.1"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="1. loop invariant preservation"
......@@ -981,7 +981,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter prime_numbers.1"
name="WP_parameter prime_numbers.38.1.1"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="1."
......@@ -1001,7 +1001,7 @@
</proof>
</goal>
<goal
name="WP_parameter prime_numbers.2"
name="WP_parameter prime_numbers.38.1.2"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="2."
......@@ -1021,7 +1021,7 @@
</proof>
</goal>
<goal
name="WP_parameter prime_numbers.3"
name="WP_parameter prime_numbers.38.1.3"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="3."
......@@ -1041,7 +1041,7 @@
</proof>
</goal>
<goal
name="WP_parameter prime_numbers.4"
name="WP_parameter prime_numbers.38.1.4"
locfile="../knuth_prime_numbers.mlw"
loclnum="63" loccnumb="6" loccnume="19"
expl="4."
......
......@@ -207,7 +207,7 @@
proved="true"
expanded="true">
<goal
name="WP_parameter maximum.1"
name="WP_parameter maximum.7.1"
locfile="../max_matrix.mlw"
loclnum="148" loccnumb="10" loccnume="17"
expl="1."
......@@ -227,7 +227,7 @@
</proof>
</goal>
<goal
name="WP_parameter maximum.2"
name="WP_parameter maximum.7.2"
locfile="../max_matrix.mlw"
loclnum="148" loccnumb="10" loccnume="17"
expl="2."
......@@ -361,7 +361,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter memo.1"
name="WP_parameter memo.1.1"
locfile="../max_matrix.mlw"
loclnum="177" loccnumb="7" loccnume="11"
expl="1."
......@@ -381,7 +381,7 @@
</proof>
</goal>
<goal
name="WP_parameter memo.2"
name="WP_parameter memo.1.2"
locfile="../max_matrix.mlw"
loclnum="177" loccnumb="7" loccnume="11"
expl="2."
......@@ -511,7 +511,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter maxmat.1"
name="WP_parameter maxmat.1.1"
locfile="../max_matrix.mlw"
loclnum="183" loccnumb="6" loccnume="12"
expl="1. assertion"
......@@ -548,7 +548,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter maxmat.1"
name="WP_parameter maxmat.2.1"
locfile="../max_matrix.mlw"
loclnum="183" loccnumb="6" loccnume="12"
expl="1. precondition"
......@@ -563,7 +563,7 @@
proved="true"
expanded="false">
<goal
name="WP_parameter maxmat.1"
name="WP_parameter maxmat.2.1.1"
locfile="../max_matrix.mlw"
loclnum="183" loccnumb="6" loccnume="12"
expl="1."
......@@ -583,7 +583,7 @@
</proof>
</goal>
<goal