Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
a0279278
Commit
a0279278
authored
Apr 25, 2014
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
replay obsolete sessions
parent
7fdb671e
Changes
101
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
101 changed files
with
6910 additions
and
7016 deletions
+6910
-7016
examples/add_list/why3session.xml
examples/add_list/why3session.xml
+4
-4
examples/algo63/why3session.xml
examples/algo63/why3session.xml
+253
-253
examples/algo64/why3session.xml
examples/algo64/why3session.xml
+18
-18
examples/algo65/why3session.xml
examples/algo65/why3session.xml
+42
-42
examples/arm/why3session.xml
examples/arm/why3session.xml
+18
-18
examples/assigning_meanings_to_programs/why3session.xml
examples/assigning_meanings_to_programs/why3session.xml
+2
-2
examples/balance/why3session.xml
examples/balance/why3session.xml
+41
-41
examples/bellman_ford/why3session.xml
examples/bellman_ford/why3session.xml
+97
-97
examples/binary_search/why3session.xml
examples/binary_search/why3session.xml
+28
-28
examples/binary_sqrt/why3session.xml
examples/binary_sqrt/why3session.xml
+17
-17
examples/bresenham/why3session.xml
examples/bresenham/why3session.xml
+9
-9
examples/bts/13375/why3session.xml
examples/bts/13375/why3session.xml
+1
-1
examples/bts/13853/why3session.xml
examples/bts/13853/why3session.xml
+2
-2
examples/bts/fsetint/why3session.xml
examples/bts/fsetint/why3session.xml
+3
-3
examples/checking_a_large_routine/why3session.xml
examples/checking_a_large_routine/why3session.xml
+16
-16
examples/conjugate/why3session.xml
examples/conjugate/why3session.xml
+30
-30
examples/counting_sort/why3session.xml
examples/counting_sort/why3session.xml
+152
-152
examples/decrease1/why3session.xml
examples/decrease1/why3session.xml
+27
-27
examples/defunctionalization/why3session.xml
examples/defunctionalization/why3session.xml
+236
-181
examples/dfa_example/why3session.xml
examples/dfa_example/why3session.xml
+25
-25
examples/dijkstra/why3session.xml
examples/dijkstra/why3session.xml
+54
-54
examples/division/why3session.xml
examples/division/why3session.xml
+5
-5
examples/edit_distance/why3session.xml
examples/edit_distance/why3session.xml
+67
-67
examples/euler002/why3session.xml
examples/euler002/why3session.xml
+21
-21
examples/ewd673/why3session.xml
examples/ewd673/why3session.xml
+1
-1
examples/fact/why3session.xml
examples/fact/why3session.xml
+10
-10
examples/fib_memo/why3session.xml
examples/fib_memo/why3session.xml
+6
-6
examples/fibonacci/why3session.xml
examples/fibonacci/why3session.xml
+36
-36
examples/fill/why3session.xml
examples/fill/why3session.xml
+1
-1
examples/find/why3session.xml
examples/find/why3session.xml
+50
-50
examples/flag/why3session.xml
examples/flag/why3session.xml
+38
-38
examples/flag2/why3session.xml
examples/flag2/why3session.xml
+38
-38
examples/foveoos11-cm/array_max/why3session.xml
examples/foveoos11-cm/array_max/why3session.xml
+1
-1
examples/foveoos11-cm/duplets/why3session.xml
examples/foveoos11-cm/duplets/why3session.xml
+2
-2
examples/foveoos11-cm/tree_max/why3session.xml
examples/foveoos11-cm/tree_max/why3session.xml
+2
-2
examples/foveoos11_challenge1/why3session.xml
examples/foveoos11_challenge1/why3session.xml
+13
-13
examples/foveoos11_challenge2/why3session.xml
examples/foveoos11_challenge2/why3session.xml
+2
-2
examples/foveoos11_challenge3/why3session.xml
examples/foveoos11_challenge3/why3session.xml
+44
-44
examples/gcd/why3session.xml
examples/gcd/why3session.xml
+45
-45
examples/gcd_bezout/why3session.xml
examples/gcd_bezout/why3session.xml
+11
-11
examples/generate_all_trees/why3session.xml
examples/generate_all_trees/why3session.xml
+53
-53
examples/hashtbl_impl/why3session.xml
examples/hashtbl_impl/why3session.xml
+78
-78
examples/hoare_logic/wp2/why3session.xml
examples/hoare_logic/wp2/why3session.xml
+33
-33
examples/insertion_sort/why3session.xml
examples/insertion_sort/why3session.xml
+59
-59
examples/insertion_sort_list/why3session.xml
examples/insertion_sort_list/why3session.xml
+16
-16
examples/insertion_sort_naive/why3session.xml
examples/insertion_sort_naive/why3session.xml
+126
-126
examples/isqrt/why3session.xml
examples/isqrt/why3session.xml
+19
-19
examples/kmp/why3session.xml
examples/kmp/why3session.xml
+78
-78
examples/knuth_prime_numbers/why3session.xml
examples/knuth_prime_numbers/why3session.xml
+552
-552
examples/largest_prime_factor/why3session.xml
examples/largest_prime_factor/why3session.xml
+69
-69
examples/lcp/why3session.xml
examples/lcp/why3session.xml
+14
-14
examples/linked_list_rev/why3session.xml
examples/linked_list_rev/why3session.xml
+20
-20
examples/max_matrix/why3session.xml
examples/max_matrix/why3session.xml
+37
-37
examples/maximum_subarray/why3session.xml
examples/maximum_subarray/why3session.xml
+230
-230
examples/mccarthy/why3session.xml
examples/mccarthy/why3session.xml
+8
-8
examples/mergesort_array/why3session.xml
examples/mergesort_array/why3session.xml
+312
-312
examples/mergesort_list/why3session.xml
examples/mergesort_list/why3session.xml
+261
-261
examples/mergesort_queue/why3session.xml
examples/mergesort_queue/why3session.xml
+93
-93
examples/mjrty/why3session.xml
examples/mjrty/why3session.xml
+26
-26
examples/muller/why3session.xml
examples/muller/why3session.xml
+21
-21
examples/my_cosine/why3session.xml
examples/my_cosine/why3session.xml
+6
-6
examples/optimal_replay/why3session.xml
examples/optimal_replay/why3session.xml
+29
-29
examples/power/why3session.xml
examples/power/why3session.xml
+13
-13
examples/queens/why3session.xml
examples/queens/why3session.xml
+705
-873
examples/quicksort/why3session.xml
examples/quicksort/why3session.xml
+249
-249
examples/relabel/why3session.xml
examples/relabel/why3session.xml
+8
-8
examples/remove_duplicate/why3session.xml
examples/remove_duplicate/why3session.xml
+72
-72
examples/residual/why3session.xml
examples/residual/why3session.xml
+36
-36
examples/resizable_array/why3session.xml
examples/resizable_array/why3session.xml
+7
-7
examples/ropes/why3session.xml
examples/ropes/why3session.xml
+308
-308
examples/same_fringe/why3session.xml
examples/same_fringe/why3session.xml
+25
-25
examples/selection_sort/why3session.xml
examples/selection_sort/why3session.xml
+36
-36
examples/sf/why3session.xml
examples/sf/why3session.xml
+24
-24
examples/snapshotable_trees/why3session.xml
examples/snapshotable_trees/why3session.xml
+28
-28
examples/sorted_list/why3session.xml
examples/sorted_list/why3session.xml
+2
-2
examples/sudoku/why3session.xml
examples/sudoku/why3session.xml
+111
-111
examples/sum_of_digits/why3session.xml
examples/sum_of_digits/why3session.xml
+35
-35
examples/there_and_back_again/why3session.xml
examples/there_and_back_again/why3session.xml
+29
-29
examples/tortoise_and_hare/why3session.xml
examples/tortoise_and_hare/why3session.xml
+5
-5
examples/tower_of_hanoi/why3session.xml
examples/tower_of_hanoi/why3session.xml
+51
-51
examples/toy_compiler/why3session.xml
examples/toy_compiler/why3session.xml
+13
-13
examples/unraveling_a_card_trick/why3session.xml
examples/unraveling_a_card_trick/why3session.xml
+69
-69
examples/vacid_0_binary_heaps/proofs/why3session.xml
examples/vacid_0_binary_heaps/proofs/why3session.xml
+156
-156
examples/vacid_0_build_maze/why3session.xml
examples/vacid_0_build_maze/why3session.xml
+24
-24
examples/vacid_0_red_black_trees/why3session.xml
examples/vacid_0_red_black_trees/why3session.xml
+356
-356
examples/vacid_0_sparse_array/why3session.xml
examples/vacid_0_sparse_array/why3session.xml
+23
-23
examples/verifythis_PrefixSumRec/why3session.xml
examples/verifythis_PrefixSumRec/why3session.xml
+117
-117
examples/verifythis_fm2012_LRS/why3session.xml
examples/verifythis_fm2012_LRS/why3session.xml
+138
-138
examples/verifythis_fm2012_treedel/why3session.xml
examples/verifythis_fm2012_treedel/why3session.xml
+43
-43
examples/vstte10_aqueue/why3session.xml
examples/vstte10_aqueue/why3session.xml
+8
-8
examples/vstte10_inverting/why3session.xml
examples/vstte10_inverting/why3session.xml
+36
-36
examples/vstte10_max_sum/why3session.xml
examples/vstte10_max_sum/why3session.xml
+29
-29
examples/vstte10_queens/why3session.xml
examples/vstte10_queens/why3session.xml
+10
-10
examples/vstte10_search_list/why3session.xml
examples/vstte10_search_list/why3session.xml
+16
-16
examples/vstte12_bfs/why3session.xml
examples/vstte12_bfs/why3session.xml
+198
-198
examples/vstte12_combinators/why3session.xml
examples/vstte12_combinators/why3session.xml
+85
-85
examples/vstte12_ring_buffer/why3session.xml
examples/vstte12_ring_buffer/why3session.xml
+95
-95
examples/vstte12_tree_reconstruction/why3session.xml
examples/vstte12_tree_reconstruction/why3session.xml
+75
-75
examples/vstte12_two_way_sort/why3session.xml
examples/vstte12_two_way_sort/why3session.xml
+28
-28
examples/zeros/why3session.xml
examples/zeros/why3session.xml
+11
-11
lib/why3/array/why3session.xml
lib/why3/array/why3session.xml
+28
-21
No files found.
examples/add_list/why3session.xml
View file @
a0279278
...
...
@@ -35,7 +35,7 @@
locfile=
"../add_list.mlw"
loclnum=
"32"
loccnumb=
"8"
loccnume=
"11"
expl=
"VC for sum"
sum=
"0a
492f8ad504c050cdce87f294c7e321
"
sum=
"0a
d629c2956d434cdf621a03e0b7c7ba
"
proved=
"true"
expanded=
"true"
shape=
"Cainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aNilCainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aIntegerVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0aRealVV1Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FACfaNilainfix =V7V2aConswVV0aConsVVV0F"
>
...
...
@@ -71,7 +71,7 @@
locfile=
"../add_list.mlw"
loclnum=
"45"
loccnumb=
"4"
loccnume=
"8"
expl=
"VC for main"
sum=
"
e4ee17c3f0db6f44050cfe5e902ce0cf
"
sum=
"
6b4e350cd7d1b4015bab61dc01e96aec
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil"
>
...
...
@@ -106,7 +106,7 @@
locfile=
"../add_list.mlw"
loclnum=
"64"
loccnumb=
"4"
loccnume=
"7"
expl=
"VC for sum"
sum=
"
0f9b53b209abc77940c4947079bdeb93
"
sum=
"
82f58e47d4e58d15d59a87efee2a6ad8
"
proved=
"true"
expanded=
"true"
shape=
"ifCainfix =V2aadd_realV0Aainfix =V3aadd_intV0aNilCfaNilainfix =V8V7aConswVV1Aainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaIntegerVVCfaNilainfix =V13V12aConswVV1Aainfix =ainfix +.V11aadd_realV12aadd_realV0Aainfix =ainfix +V3aadd_intV12aadd_intV0Iainfix =V12V10FIainfix =V11ainfix +.V2V9FaConsaRealVVV1tIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F"
>
...
...
@@ -134,7 +134,7 @@
locfile=
"../add_list.mlw"
loclnum=
"88"
loccnumb=
"4"
loccnume=
"8"
expl=
"VC for main"
sum=
"
bd44a1ba46c51b25c11a2cfdaf1b3abd
"
sum=
"
9051692e9ac1a4d1f56386a0fd7d440f
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V2c4.7Aainfix =V1c22Iainfix =V2aadd_realV0Aainfix =V1aadd_intV0FLaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNil"
>
...
...
examples/algo63/why3session.xml
View file @
a0279278
This source diff could not be displayed because it is too large. You can
view the blob
instead.
examples/algo64/why3session.xml
View file @
a0279278
...
...
@@ -20,7 +20,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"VC for quicksort"
sum=
"
a0ba4e5c3604987c94637a32a37c6bda
"
sum=
"
b3c80285a2f93720ffbeec07fe9484f7
"
proved=
"true"
expanded=
"true"
shape=
"iasorted_subV1V2ainfix +V3c1Aapermut_subV4V4V2ainfix +V3c1asorted_subV11V2ainfix +V3c1Aapermut_subV4V12V2ainfix +V3c1Aaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FAainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Aaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FAainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Aainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FAainfix <V3V0Aainfix <V2V3Aainfix <=c0V2ainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -35,7 +35,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"1. precondition"
sum=
"
e1f73adaa81d119e1d0e5773a0d17f31
"
sum=
"
60641f0dd6fd791e2eb04365466e4b67
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -55,7 +55,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"2. variant decrease"
sum=
"
7dc1c60e6b6c8e90e40cffb3c0046c34
"
sum=
"
d044cdfb327536252d9d35d6c8c8d779
"
proved=
"true"
expanded=
"false"
shape=
"variant decreaseainfix <ainfix -V5V2ainfix -V3V2Aainfix <=c0ainfix -V3V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -75,7 +75,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"3. precondition"
sum=
"
a4143c4e9e45f69e96a27ce50d7066c8
"
sum=
"
c51bbed49cb41b5186ee449ca22b5d0f
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V9c42Iainfix <=V9V3Aainfix <=V6V9FAainfix =agetV7V10c42Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11c42Iainfix <=V11V5Aainfix <=V2V11FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -95,7 +95,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"4. assertion"
sum=
"
d1e7f5d1a857b4c812defb559b1e2e12
"
sum=
"
a62cc8ba874159b234bb59428fe08b3c
"
proved=
"true"
expanded=
"false"
shape=
"assertionaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -115,7 +115,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"5. variant decrease"
sum=
"
9a0ba93f55083b56dc73b11952971e5d
"
sum=
"
cbc7bedb98f7451986a3718eda496a7c
"
proved=
"true"
expanded=
"false"
shape=
"variant decreaseainfix <ainfix -V3V6ainfix -V3V2Aainfix <=c0ainfix -V3V2Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -135,7 +135,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"6. precondition"
sum=
"
4cf9a6d2fbf230655e81bd9e1077f30c
"
sum=
"
fff053c1414e1610d034118e841c6500
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V11c42Iainfix <=V11V3Aainfix <=V6V11FAainfix =agetV7V12c42Iainfix <V12V6Aainfix <V5V12FAainfix <=agetV7V13c42Iainfix <=V13V5Aainfix <=V2V13FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -155,7 +155,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"7. assertion"
sum=
"
d66e4148760aa8026127ff6e67f9f59e
"
sum=
"
c286faac90136a80939022ab618896af
"
proved=
"true"
expanded=
"false"
shape=
"assertionaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -175,7 +175,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"8. postcondition"
sum=
"
d4f1cbfd97104fff5b918b4646fa6ebd
"
sum=
"
bf52bb94f3ce94cc8aeb29cfbd99aba5
"
proved=
"true"
expanded=
"false"
shape=
"postconditionapermut_subV4V12V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -195,7 +195,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"9. postcondition"
sum=
"
60389eea36e3a45af340b262fedda9b3
"
sum=
"
97cc3e363dcba7833cc03add00eca267
"
proved=
"true"
expanded=
"false"
shape=
"postconditionasorted_subV11V2ainfix +V3c1Iaqs_partitionV10V12V2V3V6V5c42Iasorted_subV11V6ainfix +V3c1Aapermut_subV10V12V6ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V11FIainfix <V3V0Aainfix <=V6V3Aainfix <=c0V6Iaqs_partitionV8V10V2V3V6V5c42Iasorted_subV9V2ainfix +V5c1Aapermut_subV8V10V2ainfix +V5c1Aainfix <=c0V0Lamk arrayV0V9FIainfix <V5V0Aainfix <=V2V5Aainfix <=c0V2Iainfix >=agetV7V13c42Iainfix <=V13V3Aainfix <=V6V13FAainfix =agetV7V14c42Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15c42Iainfix <=V15V5Aainfix <=V2V15FAapermut_subV4V8V2ainfix +V3c1Aainfix <=V6V3Aainfix <V5V6Aainfix <=V2V5Aainfix <=c0V0Lamk arrayV0V7FIainfix <V3V0Aainfix <V2V3Aainfix <=c0V2Iainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -215,7 +215,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"10. postcondition"
sum=
"
aae5b53b9239e2569042d779508c7be5
"
sum=
"
16dcef28364b3606b5af7ea67b96d36c
"
proved=
"true"
expanded=
"false"
shape=
"postconditionapermut_subV4V4V2ainfix +V3c1INainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -235,7 +235,7 @@
locfile=
"../algo64.mlw"
loclnum=
"42"
loccnumb=
"10"
loccnume=
"19"
expl=
"11. postcondition"
sum=
"
8db76749bdd5a917d54bd193ed583d46
"
sum=
"
a2af1e38ef1266733de9df088d4b57d3
"
proved=
"true"
expanded=
"false"
shape=
"postconditionasorted_subV1V2ainfix +V3c1INainfix <V2V3Iainfix <V3V0Aainfix <=V2V3Aainfix <=c0V2Aainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -257,7 +257,7 @@
locfile=
"../algo64.mlw"
loclnum=
"58"
loccnumb=
"6"
loccnume=
"8"
expl=
"VC for qs"
sum=
"
2f0ea9a2f922d98d2f297799012fc43d
"
sum=
"
c020ba36a9f1cbc706a81299d7e67dc5
"
proved=
"true"
expanded=
"false"
shape=
"iasorted_subV1c0V0Aapermut_allV2V2asorted_subV4c0V0Aapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FAainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1ainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -272,7 +272,7 @@
locfile=
"../algo64.mlw"
loclnum=
"58"
loccnumb=
"6"
loccnume=
"8"
expl=
"1. precondition"
sum=
"
8c00f6934f65e9c39f9c09ab73f91279
"
sum=
"
af20b26413ca9ad74cd53bb91ad9bf58
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -292,7 +292,7 @@
locfile=
"../algo64.mlw"
loclnum=
"58"
loccnumb=
"6"
loccnume=
"8"
expl=
"2. postcondition"
sum=
"
01286808ec84d087a5a4b8d7536d0734
"
sum=
"
8c72e4401654ed269af73c95614802d2
"
proved=
"true"
expanded=
"false"
shape=
"postconditionapermut_allV2V5Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FIainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -312,7 +312,7 @@
locfile=
"../algo64.mlw"
loclnum=
"58"
loccnumb=
"6"
loccnume=
"8"
expl=
"3. postcondition"
sum=
"
703f39eec05db1f34c5aa54e58f9632b
"
sum=
"
abf810b8c32150c26b4a3f3e6aacac6e
"
proved=
"true"
expanded=
"false"
shape=
"postconditionasorted_subV4c0V0Iasorted_subV4c0ainfix +V3c1Aapermut_subV2V5c0ainfix +V3c1Aainfix <=c0V0Lamk arrayV0V4FIainfix <V3V0Aainfix <=c0V3Aainfix <=c0c0Lainfix -V0c1Iainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -332,7 +332,7 @@
locfile=
"../algo64.mlw"
loclnum=
"58"
loccnumb=
"6"
loccnume=
"8"
expl=
"4. postcondition"
sum=
"
61ef3b42c571d3266a8f4837e66b5612
"
sum=
"
ba4a3b43dca6859d783d70d4c5b16669
"
proved=
"true"
expanded=
"false"
shape=
"postconditionapermut_allV2V2INainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F"
>
...
...
@@ -352,7 +352,7 @@
locfile=
"../algo64.mlw"
loclnum=
"58"
loccnumb=
"6"
loccnume=
"8"
expl=
"5. postcondition"
sum=
"
187fbbba680280cd5e202e8e201c087
f"
sum=
"
8532155787a9b770710dad8ca4324c1
f"
proved=
"true"
expanded=
"false"
shape=
"postconditionasorted_subV1c0V0INainfix >V0c0Iainfix <=c0V0Lamk arrayV0V1F"
>
...
...
examples/algo65/why3session.xml
View file @
a0279278
This diff is collapsed.
Click to expand it.
examples/arm/why3session.xml
View file @
a0279278
...
...
@@ -28,7 +28,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"VC for insertion_sort"
sum=
"
06febdbfc8bb8fcf0669068b174ab836
"
sum=
"
12ad10e0643d819dcdf614beb2a7db7f
"
proved=
"true"
expanded=
"false"
shape=
"iainfix <=V6c45Aainfix =V7c9Aainfix <=c0V0iainfix <ainfix -c10V16ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V16c2ainfix -V16c1Aainfix =V10ainfix -V16c2AainvV14Aainfix <=V16c11Aainfix <=c2V16Iainfix =V16ainfix +V5c1Fainfix <V22V11Aainfix <=c0V11Aainfix <=ainfix *c2V17ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V22Aainvamk arrayV0V21Aainfix <=V22V5Aainfix <=c1V22Iainfix =V22ainfix -V11c1FIainfix =V21asetV19V20agetV13V11Aainfix <=c0V0FAainfix <V20V0Aainfix <=c0V20Lainfix -V11c1Iainfix =V19asetV13V11agetV13V18Aainfix <=c0V0FAainfix <V11V0Aainfix <=c0V11Aainfix <V18V0Aainfix <=c0V18Lainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V17ainfix +V12c1Fainfix <agetV13V11agetV13V15Aainfix <V11V0Aainfix <=c0V11Aainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -43,7 +43,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"1. loop invariant init"
sum=
"
8cf87b3e070181b8fb5eb9cdbb7b1dc2
"
sum=
"
62cedfa9a8840be299dc60f48e358e9d
"
proved=
"true"
expanded=
"false"
shape=
"loop invariant initainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -63,7 +63,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"2. loop invariant init"
sum=
"
ef3a262df36efc96b1d4f339584dfe21
"
sum=
"
b847af6941605e2d7d0f84017c990223
"
proved=
"true"
expanded=
"false"
shape=
"loop invariant initainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -83,7 +83,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"3. type invariant"
sum=
"f
626a1b9f59d904def75836988e58226
"
sum=
"f
d006cfa55f9c725523fa4d12ca78e01
"
proved=
"true"
expanded=
"false"
shape=
"type invariantainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -103,7 +103,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"4. index in array bounds"
sum=
"
ae3ec21ef89e4896a228767889d9460a
"
sum=
"
f227e497d584beb98543bab70b47919b
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <V15V0Aainfix <=c0V15Iainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -123,7 +123,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"5. index in array bounds"
sum=
"
290e68b7c44ac78171d54c0bdadae74c
"
sum=
"
ba9aa8802c1c8bbb7224a4ff9eb6cb57
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -143,7 +143,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"6. index in array bounds"
sum=
"
9e7132818779fe98d03e10258cc0089c
"
sum=
"
d5a19d25ce8ded0495d70f00972b3a9a
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <V11V0Aainfix <=c0V11Iainfix =V16ainfix +V12c1FIainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -163,7 +163,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"7. index in array bounds"
sum=
"
848239a95808b61279571abe88004d80
"
sum=
"
9bff97babe4eca7f0409aed0b47935ec
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <V17V0Aainfix <=c0V17Lainfix -V11c1Iainfix <V11V0Aainfix <=c0V11Iainfix =V16ainfix +V12c1FIainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -183,7 +183,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"8. index in array bounds"
sum=
"
1d4e96d179c604f72fda80210f9f6785
"
sum=
"
d24f30ba4db1835ea6c7cbe67360299b
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <V11V0Aainfix <=c0V11Iainfix <V17V0Aainfix <=c0V17Lainfix -V11c1Iainfix <V11V0Aainfix <=c0V11Iainfix =V16ainfix +V12c1FIainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -203,7 +203,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"9. index in array bounds"
sum=
"
0980c1893e6a9b4ee02e907e32e34df4
"
sum=
"
891cbbbe7c1a5380ce4c569a6fab8ff3
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <V19V0Aainfix <=c0V19Lainfix -V11c1Iainfix =V18asetV13V11agetV13V17Aainfix <=c0V0FIainfix <V11V0Aainfix <=c0V11Iainfix <V17V0Aainfix <=c0V17Lainfix -V11c1Iainfix <V11V0Aainfix <=c0V11Iainfix =V16ainfix +V12c1FIainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -223,7 +223,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"10. loop invariant preservation"
sum=
"
e6c601832c55c07cc344f13d32106a16
"
sum=
"
2c65e9965e0b58c50e58909f7dce52b4
"
proved=
"true"
expanded=
"false"
shape=
"loop invariant preservationainfix <=ainfix *c2V16ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V21Aainvamk arrayV0V20Aainfix <=V21V5Aainfix <=c1V21Iainfix =V21ainfix -V11c1FIainfix =V20asetV18V19agetV13V11Aainfix <=c0V0FIainfix <V19V0Aainfix <=c0V19Lainfix -V11c1Iainfix =V18asetV13V11agetV13V17Aainfix <=c0V0FIainfix <V11V0Aainfix <=c0V11Iainfix <V17V0Aainfix <=c0V17Lainfix -V11c1Iainfix <V11V0Aainfix <=c0V11Iainfix =V16ainfix +V12c1FIainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -243,7 +243,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"11. loop variant decrease"
sum=
"
58e5700a1f33cc3fd3377843a3913b8c
"
sum=
"
c40f38c738ab3c9bf180ca851f10dd2f
"
proved=
"true"
expanded=
"false"
shape=
"loop variant decreaseainfix <V21V11Aainfix <=c0V11Iainfix =V21ainfix -V11c1FIainfix =V20asetV18V19agetV13V11Aainfix <=c0V0FIainfix <V19V0Aainfix <=c0V19Lainfix -V11c1Iainfix =V18asetV13V11agetV13V17Aainfix <=c0V0FIainfix <V11V0Aainfix <=c0V11Iainfix <V17V0Aainfix <=c0V17Lainfix -V11c1Iainfix <V11V0Aainfix <=c0V11Iainfix =V16ainfix +V12c1FIainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -263,7 +263,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"12. loop invariant preservation"
sum=
"
9e02b7b4d04c96e667451d8e09465954
"
sum=
"
40978b8820a2223fa24e995db5f1e9d1
"
proved=
"true"
expanded=
"false"
shape=
"loop invariant preservationainfix <=ainfix *c2V12ainfix *ainfix -V16c2ainfix -V16c1Aainfix =V10ainfix -V16c2AainvV14Aainfix <=V16c11Aainfix <=c2V16Iainfix =V16ainfix +V5c1FINainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -283,7 +283,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"13. loop variant decrease"
sum=
"
5fdee6c3110ba46b748158865658ff11
"
sum=
"
a686ac7bc009cdbf8c7721f8c222cb8d
"
proved=
"true"
expanded=
"false"
shape=
"loop variant decreaseainfix <ainfix -c10V16ainfix -c10V5Aainfix <=c0ainfix -c10V5Iainfix =V16ainfix +V5c1FINainfix <agetV13V11agetV13V15Iainfix <V11V0Aainfix <=c0V11Iainfix <V15V0Aainfix <=c0V15Aainfix <=c0V0Lainfix -V11c1Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FIainfix =V10ainfix +V7c1FIainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -303,7 +303,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"14. type invariant"
sum=
"
bab51a0983af4b2143828fcf7a3c7912
"
sum=
"
419004f397624b7907de99cc5f139e80
"
proved=
"true"
expanded=
"false"
shape=
"type invariantainfix <=c0V0INainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -323,7 +323,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"15. postcondition"
sum=
"
84650f4a259d4767a0fcaf58c821f2ce
"
sum=
"
16ba8ad695c6d82d3bde615f6426d0a2
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix <=V6c45Aainfix =V7c9Iainfix <=c0V0INainfix <=V5c10Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FIainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF"
>
...
...
@@ -359,7 +359,7 @@
locfile=
"../arm.mlw"
loclnum=
"120"
loccnumb=
"6"
loccnume=
"18"
expl=
"VC for path_init_l2"
sum=
"
b1e6332cf78bce93567776b299146375
"
sum=
"
ddaf1b23f084f36f71d149a56e4c5a17
"
proved=
"true"
expanded=
"false"
shape=
"ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F"
>
...
...
@@ -387,7 +387,7 @@
locfile=
"../arm.mlw"
loclnum=
"127"
loccnumb=
"6"
loccnume=
"18"
expl=
"VC for path_l2_exit"
sum=
"
d10152cbb8b048fc4c8f4bc2867440e
4"
sum=
"
eb7cf7cf9c33eb25d306a2663432ef0
4"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V0c9Iainfix =V4aFalseIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F"
>
...
...
examples/assigning_meanings_to_programs/why3session.xml
View file @
a0279278
...
...
@@ -24,7 +24,7 @@
locfile=
"../assigning_meanings_to_programs.mlw"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for sum"
sum=
"
329d3acbda193f226c9e300474bf832a
"
sum=
"
08be4365a1bbf3642e32e902d58a4e3c
"
proved=
"true"
expanded=
"true"
shape=
"iainfix =V3asumV1c1ainfix +V2c1ainfix <ainfix -V2V6ainfix -V2V4Aainfix <=c0ainfix -V2V4Aainfix =V5asumV1c1V6Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV1V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V2Iainfix =V3asumV1c1V4Aainfix <=V4ainfix +V2c1Aainfix <=c1V4FAainfix =c0asumV1c1c1Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Aainfix <=c0V2Aainfix <=c0V0F"
>
...
...
@@ -51,7 +51,7 @@
locfile=
"../assigning_meanings_to_programs.mlw"
loclnum=
"38"
loccnumb=
"6"
loccnume=
"14"
expl=
"VC for division"
sum=
"
188bd14860a30ee027c058f8c34ad87a
"
sum=
"
5a077cf4ab2c23e67ed74619034dc338
"
proved=
"true"
expanded=
"true"
shape=
"iainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix >=V2V1Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0F"
>
...
...
examples/balance/why3session.xml
View file @
a0279278
...
...
@@ -20,22 +20,22 @@
<theory
name=
"Roberval"
locfile=
"../balance.mlw"
loclnum=
"
8
"
loccnumb=
"7"
loccnume=
"15"
loclnum=
"
10
"
loccnumb=
"7"
loccnume=
"15"
verified=
"true"
expanded=
"false"
>
</theory>
<theory
name=
"Puzzle8"
locfile=
"../balance.mlw"
loclnum=
"4
3
"
loccnumb=
"7"
loccnume=
"14"
loclnum=
"4
5
"
loccnumb=
"7"
loccnume=
"14"
verified=
"true"
expanded=
"false"
>
<goal
name=
"WP_parameter solve3"
locfile=
"../balance.mlw"
loclnum=
"5
7
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"5
9
"
loccnumb=
"6"
loccnume=
"12"
expl=
"VC for solve3"
sum=
"
27473b276e8ad85573bf61ca7992e027
"
sum=
"
b99690f38a8859fcbc376bfe11476985
"
proved=
"true"
expanded=
"false"
shape=
"Cainfix =V9ainfix -V5c1Aainfix =V2V3aRightainfix =V9ainfix -V5c1Aainfix =ainfix +V2c1V3aLeftainfix =V9ainfix -V5c1Aainfix =ainfix +V2c2V3aEqualV10Iainfix =V9ainfix -V5c1ACainfix >V8V7aLeftainfix =V8V7aEqualainfix <V8V7aRightV10FFAainfix >V5c0LagetV1V2Aainfix <V2V0Aainfix <=c0V2LagetV1V6Aainfix <V6V0Aainfix <=c0V6Lainfix +V2c1Iaspecamk arrayV0V1V2ainfix +V2c3V3V4Aainfix >=V5c1Aainfix <=c0V0FF"
>
...
...
@@ -61,9 +61,9 @@
<goal
name=
"WP_parameter solve8"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"VC for solve8"
sum=
"
390784e66f3947429669e6772f3d668e
"
sum=
"
9841fc04de124860d6dbeb8c34375b9a
"
proved=
"true"
expanded=
"false"
shape=
"CaspecV4c0ainfix +c0c3V2V3Aainfix >=V8c1aRightaspecV4c3ainfix +c3c3V2V3Aainfix >=V8c1aLeftCainfix =c6V2aRightainfix =c7V2wV13Iainfix =V12ainfix -V8c1ACainfix >V11V10aLeftainfix =V11V10aEqualainfix <V11V10aRightV13FFAainfix >V8c0LagetV1c6Aainfix <c6V0Aainfix <=c0c6LagetV1c7Aainfix <c7V0Aainfix <=c0c7aEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFAainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Aainfix <c0V0Aainfix <=c0c0Aainfix <c1V0Aainfix <=c0c1Aainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Aainfix <c3V0Aainfix <=c0c3Aainfix <c4V0Aainfix <=c0c4Aainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -76,9 +76,9 @@
<goal
name=
"WP_parameter solve8.1"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"1. index in array bounds"
sum=
"e
eedfe7554063317ba6950ff2bdc41e0
"
sum=
"e
8636c6042a6fbb5009ffcaaf3a51728
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -104,9 +104,9 @@
<goal
name=
"WP_parameter solve8.2"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"2. index in array bounds"
sum=
"
567e12e52df66916d63d7da21bf91f1f
"
sum=
"
a719814bcc87c5699bcf9f906a0549dc
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -132,9 +132,9 @@
<goal
name=
"WP_parameter solve8.3"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"3. index in array bounds"
sum=
"
02ac3d7fb3c30fad08e6fa6c057fc559
"
sum=
"
aeaa011af7aadec3b5d860be903d6d84
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -160,9 +160,9 @@
<goal
name=
"WP_parameter solve8.4"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"4. index in array bounds"
sum=
"
e7d856d4522848a97aa9f26bf0cf9a70
"
sum=
"
c7777f8b4f60d2f52579220995ba1901
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -188,9 +188,9 @@
<goal
name=
"WP_parameter solve8.5"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"5. index in array bounds"
sum=
"
2007aadf9b6dd18988f67a238e5865a2
"
sum=
"
713ff67741edb2ca4f308d445dd7af57
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -216,9 +216,9 @@
<goal
name=
"WP_parameter solve8.6"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"6. index in array bounds"
sum=
"
149ac39419592955c042d2d55538a78f
"
sum=
"
b59bd221e001b77d6a83147ee7cdc84e
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -244,9 +244,9 @@
<goal
name=
"WP_parameter solve8.7"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"7. precondition"
sum=
"
06631246354762bd1389a5ba4ff04cfb
"
sum=
"
450384f15c544017e2760bb39352e02f
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -264,9 +264,9 @@
<goal
name=
"WP_parameter solve8.8"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"8. precondition"
sum=
"
c9e666c32cd96c77e05b3b40bb0c0ab6
"
sum=
"
852665f61acf27a7dd6a7ba0661fed64
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCainfix >=V8c1aRighttaLefttaEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -292,9 +292,9 @@
<goal
name=
"WP_parameter solve8.9"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"9. precondition"
sum=
"
338d14364c728747dfce59989e64d4e6
"
sum=
"
c50d4db7e5e8e3f71494ccf12e09124e
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCaspecV4c0ainfix +c0c3V2V3aRighttaLefttaEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -320,9 +320,9 @@
<goal
name=
"WP_parameter solve8.10"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"10. precondition"
sum=
"
274d13e1221df21f226e0bb942191e1b
"
sum=
"
f40c77965b3b599d0360e403bd9a64b4
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaRightainfix >=V8c1aLefttaEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -348,9 +348,9 @@
<goal
name=
"WP_parameter solve8.11"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"11. precondition"
sum=
"
3de4e187e630d54612d2eac3d08016d7
"
sum=
"
c49dd839f25c60a0d250482a4e52b6ea
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaRightaspecV4c3ainfix +c3c3V2V3aLefttaEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -376,9 +376,9 @@
<goal
name=
"WP_parameter solve8.12"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"12. index in array bounds"
sum=
"
f3db0dec21695bbf9ae89a8af002b8ee
"
sum=
"
699da9471162d3e1c4c1c07203095e21
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsCtaRighttaLeftainfix <c7V0Aainfix <=c0c7aEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -404,9 +404,9 @@
<goal
name=
"WP_parameter solve8.13"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"13. index in array bounds"
sum=
"
1ee5e9a007b5ace1557f39d97226863f
"
sum=
"
d99d36b57c8703dcb6b7ff793e47f492
"
proved=
"true"
expanded=
"false"
shape=
"index in array boundsCtaRighttaLeftainfix <c6V0Aainfix <=c0c6LagetV1c7Iainfix <c7V0Aainfix <=c0c7aEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -432,9 +432,9 @@
<goal
name=
"WP_parameter solve8.14"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"14. precondition"
sum=
"
04aa396ec5f5d7453853704af26b8b26
"
sum=
"
4cb069f2aa1ac29a15155d968c2e2801
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaRighttaLeftainfix >V8c0LagetV1c6Iainfix <c6V0Aainfix <=c0c6LagetV1c7Iainfix <c7V0Aainfix <=c0c7aEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -452,9 +452,9 @@
<goal
name=
"WP_parameter solve8.15"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"15. postcondition"
sum=
"
9fb4f0804157a53f686e3f273a34cebc
"
sum=
"
aea0af9d5bdb85dfe629ea850b6a7ece
"
proved=
"true"
expanded=
"false"
shape=
"postconditionCtaRighttaLeftCainfix =c6V2aRighttwV13Iainfix =V12ainfix -V8c1ACainfix >V11V10aLeftainfix =V11V10aEqualainfix <V11V10aRightV13FFIainfix >V8c0LagetV1c6Iainfix <c6V0Aainfix <=c0c6LagetV1c7Iainfix <c7V0Aainfix <=c0c7aEqualV9Iainfix =V8ainfix -V5c1ACainfix >V7V6aLeftainfix =V7V6aEqualainfix <V7V6aRightV9FFIainfix >V5c0Lainfix +ainfix +agetV1c0agetV1c1agetV1c2Iainfix <c0V0Aainfix <=c0c0Iainfix <c1V0Aainfix <=c0c1Iainfix <c2V0Aainfix <=c0c2Lainfix +ainfix +agetV1c3agetV1c4agetV1c5Iainfix <c3V0Aainfix <=c0c3Iainfix <c4V0Aainfix <=c0c4Iainfix <c5V0Aainfix <=c0c5IaspecV4c0c8V2V3Aainfix =V5c2Aainfix <=c0V0FLamk arrayV0V1F"
>
...
...
@@ -480,9 +480,9 @@
<goal
name=
"WP_parameter solve8.16"
locfile=
"../balance.mlw"
loclnum=
"7
1
"
loccnumb=
"6"
loccnume=
"12"
loclnum=
"7
3
"
loccnumb=
"6"
loccnume=
"12"
expl=
"16. postcondition"
sum=
"
0b5fc46a512e51825ca956792ad78fe2
"
sum=
"
450979a888923b6061e7a9e207019e40
"