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
9bf1998f
Commit
9bf1998f
authored
Aug 07, 2013
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
update sessions (in progress)
parent
ac976a84
Changes
93
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
93 changed files
with
17020 additions
and
6388 deletions
+17020
-6388
examples/algo63/why3session.xml
examples/algo63/why3session.xml
+229
-140
examples/algo64/why3session.xml
examples/algo64/why3session.xml
+13
-13
examples/algo65/why3session.xml
examples/algo65/why3session.xml
+26
-26
examples/alphaBeta/why3session.xml
examples/alphaBeta/why3session.xml
+30
-30
examples/arm/why3session.xml
examples/arm/why3session.xml
+4
-4
examples/assigning_meanings_to_programs/why3session.xml
examples/assigning_meanings_to_programs/why3session.xml
+1
-1
examples/bellman_ford/why3session.xml
examples/bellman_ford/why3session.xml
+383
-111
examples/binary_search/why3session.xml
examples/binary_search/why3session.xml
+3
-3
examples/bitvectors/bitvector/why3session.xml
examples/bitvectors/bitvector/why3session.xml
+21
-21
examples/bitvectors/double_of_int/why3session.xml
examples/bitvectors/double_of_int/why3session.xml
+327
-127
examples/bitvectors/neg_as_xor/why3session.xml
examples/bitvectors/neg_as_xor/why3session.xml
+1
-1
examples/bitvectors/power2/why3session.xml
examples/bitvectors/power2/why3session.xml
+150
-170
examples/bts/13375/why3session.xml
examples/bts/13375/why3session.xml
+1
-1
examples/bts/13853/why3session.xml
examples/bts/13853/why3session.xml
+1
-1
examples/bts/fsetint/why3session.xml
examples/bts/fsetint/why3session.xml
+3
-3
examples/check-builtin/ac/why3session.xml
examples/check-builtin/ac/why3session.xml
+1
-1
examples/check-builtin/array/why3session.xml
examples/check-builtin/array/why3session.xml
+7
-7
examples/check-builtin/bool/why3session.xml
examples/check-builtin/bool/why3session.xml
+10
-10
examples/check-builtin/int/why3session.xml
examples/check-builtin/int/why3session.xml
+216
-32
examples/check-builtin/intreal/why3session.xml
examples/check-builtin/intreal/why3session.xml
+4
-4
examples/check-builtin/minmax/why3session.xml
examples/check-builtin/minmax/why3session.xml
+1
-1
examples/check-builtin/propositional/why3session.xml
examples/check-builtin/propositional/why3session.xml
+1
-1
examples/conjugate/why3session.xml
examples/conjugate/why3session.xml
+29
-29
examples/counting_sort/why3session.xml
examples/counting_sort/why3session.xml
+265
-237
examples/decrease1/why3session.xml
examples/decrease1/why3session.xml
+27
-35
examples/dijkstra/why3session.xml
examples/dijkstra/why3session.xml
+66
-66
examples/edit_distance/why3session.xml
examples/edit_distance/why3session.xml
+66
-66
examples/f_puzzle/why3session.xml
examples/f_puzzle/why3session.xml
+58
-30
examples/fib_memo/why3session.xml
examples/fib_memo/why3session.xml
+5
-5
examples/fill/why3session.xml
examples/fill/why3session.xml
+3
-3
examples/find/why3session.xml
examples/find/why3session.xml
+50
-50
examples/flag/why3session.xml
examples/flag/why3session.xml
+32
-32
examples/flag2/why3session.xml
examples/flag2/why3session.xml
+45
-41
examples/foveoos11-cm/array_max/why3session.xml
examples/foveoos11-cm/array_max/why3session.xml
+4
-4
examples/foveoos11-cm/duplets/why3session.xml
examples/foveoos11-cm/duplets/why3session.xml
+5
-5
examples/foveoos11-cm/tree_max/why3session.xml
examples/foveoos11-cm/tree_max/why3session.xml
+3
-3
examples/foveoos11_challenge1/why3session.xml
examples/foveoos11_challenge1/why3session.xml
+13
-13
examples/foveoos11_challenge3/why3session.xml
examples/foveoos11_challenge3/why3session.xml
+49
-49
examples/gcd/why3session.xml
examples/gcd/why3session.xml
+1
-1
examples/generate_all_trees/why3session.xml
examples/generate_all_trees/why3session.xml
+80
-76
examples/hamming_sequence/why3session.xml
examples/hamming_sequence/why3session.xml
+1
-1
examples/hashtbl_impl/why3session.xml
examples/hashtbl_impl/why3session.xml
+84
-84
examples/hoare_logic/blocking_semantics5/blocking_semantics5_WP_wp_preserved_by_reduction_4.v
...ics5/blocking_semantics5_WP_wp_preserved_by_reduction_4.v
+241
-260
examples/hoare_logic/blocking_semantics5/why3session.xml
examples/hoare_logic/blocking_semantics5/why3session.xml
+882
-886
examples/hoare_logic/formula/why3session.xml
examples/hoare_logic/formula/why3session.xml
+2
-2
examples/hoare_logic/imp_n/why3session.xml
examples/hoare_logic/imp_n/why3session.xml
+51
-27
examples/hoare_logic/wp2/why3session.xml
examples/hoare_logic/wp2/why3session.xml
+73
-73
examples/insertion_sort/why3session.xml
examples/insertion_sort/why3session.xml
+59
-59
examples/insertion_sort_naive/why3session.xml
examples/insertion_sort_naive/why3session.xml
+123
-123
examples/isqrt/why3session.xml
examples/isqrt/why3session.xml
+70
-34
examples/kmp/why3session.xml
examples/kmp/why3session.xml
+78
-78
examples/knuth_prime_numbers/why3session.xml
examples/knuth_prime_numbers/why3session.xml
+3892
-78
examples/lcp/why3session.xml
examples/lcp/why3session.xml
+15
-15
examples/linked_list_rev/why3session.xml
examples/linked_list_rev/why3session.xml
+15
-15
examples/list_rev/why3session.xml
examples/list_rev/why3session.xml
+275
-55
examples/logic/agatha/why3session.xml
examples/logic/agatha/why3session.xml
+2
-2
examples/logic/einstein/why3session.xml
examples/logic/einstein/why3session.xml
+96
-68
examples/logic/explicit_subst/why3session.xml
examples/logic/explicit_subst/why3session.xml
+319
-87
examples/logic/genealogy/why3session.xml
examples/logic/genealogy/why3session.xml
+8
-8
examples/logic/lagrange_inequality/why3session.xml
examples/logic/lagrange_inequality/why3session.xml
+14
-10
examples/logic/sorted_list/why3session.xml
examples/logic/sorted_list/why3session.xml
+1
-1
examples/logic/triangle_inequality/why3session.xml
examples/logic/triangle_inequality/why3session.xml
+127
-147
examples/max_matrix/why3session.xml
examples/max_matrix/why3session.xml
+39
-39
examples/mergesort_queue/why3session.xml
examples/mergesort_queue/why3session.xml
+2
-2
examples/mjrty/why3session.xml
examples/mjrty/why3session.xml
+36
-36
examples/muller/why3session.xml
examples/muller/why3session.xml
+21
-21
examples/optimal_replay/why3session.xml
examples/optimal_replay/why3session.xml
+29
-29
examples/queens/why3session.xml
examples/queens/why3session.xml
+2629
-119
examples/quicksort/why3session.xml
examples/quicksort/why3session.xml
+37
-37
examples/resizable_array/why3session.xml
examples/resizable_array/why3session.xml
+7
-7
examples/selection_sort/why3session.xml
examples/selection_sort/why3session.xml
+24
-24
examples/sf/why3session.xml
examples/sf/why3session.xml
+76
-8
examples/tests-provers/alt-ergo-models/why3session.xml
examples/tests-provers/alt-ergo-models/why3session.xml
+1
-1
examples/tests-provers/cvc3/why3session.xml
examples/tests-provers/cvc3/why3session.xml
+1
-1
examples/tower_of_hanoi/why3session.xml
examples/tower_of_hanoi/why3session.xml
+1047
-35
examples/unraveling_a_card_trick/why3session.xml
examples/unraveling_a_card_trick/why3session.xml
+2
-2
examples/vacid_0_binary_heaps/proofs/why3session.xml
examples/vacid_0_binary_heaps/proofs/why3session.xml
+595
-611
examples/vacid_0_red_black_trees/why3session.xml
examples/vacid_0_red_black_trees/why3session.xml
+2011
-97
examples/vacid_0_sparse_array/why3session.xml
examples/vacid_0_sparse_array/why3session.xml
+24
-24
examples/verifythis_PrefixSumRec/why3session.xml
examples/verifythis_PrefixSumRec/why3session.xml
+235
-235
examples/verifythis_fm2012_LRS/why3session.xml
examples/verifythis_fm2012_LRS/why3session.xml
+476
-540
examples/verifythis_fm2012_treedel/why3session.xml
examples/verifythis_fm2012_treedel/why3session.xml
+119
-119
examples/vstte10_aqueue/why3session.xml
examples/vstte10_aqueue/why3session.xml
+15
-15
examples/vstte10_inverting/why3session.xml
examples/vstte10_inverting/why3session.xml
+69
-69
examples/vstte10_max_sum/why3session.xml
examples/vstte10_max_sum/why3session.xml
+79
-79
examples/vstte10_queens/why3session.xml
examples/vstte10_queens/why3session.xml
+14
-14
examples/vstte10_search_list/why3session.xml
examples/vstte10_search_list/why3session.xml
+17
-17
examples/vstte12_bfs/why3session.xml
examples/vstte12_bfs/why3session.xml
+196
-196
examples/vstte12_combinators/why3session.xml
examples/vstte12_combinators/why3session.xml
+148
-92
examples/vstte12_ring_buffer/why3session.xml
examples/vstte12_ring_buffer/why3session.xml
+191
-191
examples/vstte12_tree_reconstruction/why3session.xml
examples/vstte12_tree_reconstruction/why3session.xml
+156
-100
examples/vstte12_two_way_sort/why3session.xml
examples/vstte12_two_way_sort/why3session.xml
+39
-39
examples/zeros/why3session.xml
examples/zeros/why3session.xml
+23
-23
No files found.
examples/algo63/why3session.xml
View file @
9bf1998f
This diff is collapsed.
Click to expand it.
examples/algo64/why3session.xml
View file @
9bf1998f
...
...
@@ -28,7 +28,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"VC for quicksort"
sum=
"
ab2a63ccffd01ef10ebb7dc0e7571df9
"
sum=
"
58fde39b3de57a13ada8d66fc6adb75e
"
proved=
"true"
expanded=
"true"
shape=
"iasorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Aapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FAainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Aainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Aapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FAainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Aainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FAainfix <V2V0Aainfix <V1V2Aainfix <=c0V1ainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -43,7 +43,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"1. precondition"
sum=
"
153b0a4ec87c1b7e4f4d4bc2ccec7568
"
sum=
"
3c43f6f2c8269df69c948249e7e1e382
"
proved=
"true"
expanded=
"true"
shape=
"preconditionainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -63,7 +63,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"2. variant decrease"
sum=
"
d52fa8437c333e33dfcab95b688273a1
"
sum=
"
e4af12d56325fd83d45591296cbe3447
"
proved=
"true"
expanded=
"true"
shape=
"variant decreaseainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -83,7 +83,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"3. precondition"
sum=
"
d824dc170165d3d1bd7f3e8aa5e84688
"
sum=
"
6b486a7a19953085f8a449593e49e9e3
"
proved=
"true"
expanded=
"true"
shape=
"preconditionainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -103,7 +103,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"4. assertion"
sum=
"
a2985e78ef08b400f95948a9160374ea
"
sum=
"
b203e24ff20076cb2659b3454a5a6012
"
proved=
"true"
expanded=
"true"
shape=
"assertionapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -123,7 +123,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"5. variant decrease"
sum=
"
f1c89158dd889a67f6ec2b53de972207
"
sum=
"
6cf15418ef8d15af54e3962c629dabd3
"
proved=
"true"
expanded=
"true"
shape=
"variant decreaseainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -143,7 +143,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"6. precondition"
sum=
"
74c8e5dfdcaff3e9e3b7cf11e06af710
"
sum=
"
a1a8658fb645764ad38241ce182e9b8a
"
proved=
"true"
expanded=
"true"
shape=
"preconditionainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -163,7 +163,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"7. assertion"
sum=
"
ffc073f16103d696d99568ec5ba9f74a
"
sum=
"
d4c5f783e016831c9b4150a9a837996b
"
proved=
"true"
expanded=
"true"
shape=
"assertionapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -183,7 +183,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"8. postcondition"
sum=
"
08fdd2672d24fafbe0f05ee5f635f6e9
"
sum=
"
7b2272981678c505d00d003541a25323
"
proved=
"true"
expanded=
"true"
shape=
"postconditionapermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -203,7 +203,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"9. postcondition"
sum=
"3
5ebeae2f5fbe5224561cff570ab23b9
"
sum=
"3
9cbb1c21ab896a97d894567ed414a90
"
proved=
"true"
expanded=
"true"
shape=
"postconditionasorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -223,7 +223,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"
36.9
2"
/>
<result
status=
"valid"
time=
"
16.5
2"
/>
</proof>
</goal>
<goal
...
...
@@ -231,7 +231,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"10. postcondition"
sum=
"
e6bf165a8862cc0215e1fe933570e6fe
"
sum=
"
c9aee77b1de0f789e80a8d6207e238a8
"
proved=
"true"
expanded=
"true"
shape=
"postconditionapermut_subV3V3V1ainfix +V2c1INainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
@@ -251,7 +251,7 @@
locfile=
"../algo64.mlw"
loclnum=
"37"
loccnumb=
"10"
loccnume=
"19"
expl=
"11. postcondition"
sum=
"
07f6b005264964017be91678f79e1b36
"
sum=
"
324cbdea9c2d639c2179bcbffb508f78
"
proved=
"true"
expanded=
"true"
shape=
"postconditionasorted_subV3V1ainfix +V2c1INainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
examples/algo65/why3session.xml
View file @
9bf1998f
This diff is collapsed.
Click to expand it.
examples/alphaBeta/why3session.xml
View file @
9bf1998f
...
...
@@ -43,7 +43,7 @@
name=
"Test"
locfile=
"../alphaBeta.mlw"
loclnum=
"76"
loccnumb=
"7"
loccnume=
"11"
sum=
"
b97508a5e6364636f5f02cfc58030f63
"
sum=
"
f66146e79e082693b350edcf7f60f0d8
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <=aprefix -aposition_valueado_moveV0V1aminmaxV0c1IamemV1V2Lalegal_movesV0F"
>
...
...
@@ -70,14 +70,14 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
19
"
/>
<result
status=
"valid"
time=
"0.
02
"
/>
</proof>
</goal>
<goal
name=
"minmax_bound"
locfile=
"../alphaBeta.mlw"
loclnum=
"82"
loccnumb=
"8"
loccnume=
"20"
sum=
"
bbb697c0cfcf19abc3fbd55aee2bf562
"
sum=
"
5e94a9518279472d5a187393a326ef9f
"
proved=
"true"
expanded=
"false"
shape=
"ainfix <aminmaxV0V1ainfinityAainfix <aprefix -ainfinityaminmaxV0V1Iainfix >=V1c0F"
>
...
...
@@ -95,7 +95,7 @@
name=
"minmax_nomove"
locfile=
"../alphaBeta.mlw"
loclnum=
"86"
loccnumb=
"8"
loccnume=
"21"
sum=
"
0d8cf238d83e205510be29542efe826b
"
sum=
"
4d403af107fd8fb5aaf11c0a5e886a5f
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =aminmaxV0V1aposition_valueV0Iainfix =alegal_movesV0aNilAainfix >=V1c0F"
>
...
...
@@ -160,7 +160,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"VC for move_value_alpha_beta"
sum=
"
b293a359249fd530e078d35691f1fdb3
"
sum=
"
3019c70efe72aeccd36f2abd4f9508d8
"
proved=
"true"
expanded=
"false"
shape=
"iiainfix <=V10V0ainfix >=V10V1ainfix <=V11aprefix -V1ainfix =V10aprefix -V11ainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V4ainfix -V3c1Laprefix -V9Iiiainfix >=V9V7ainfix <=V9V8ainfix <=aminmaxV5V6V8ainfix =V9aminmaxV5V6ainfix <aminmaxV5V6V7Aainfix <V8aminmaxV5V6FAainfix >=V6c0Laprefix -V1Laprefix -V0Lainfix -V3c1Lado_moveV2V4Iainfix >=V3c1F"
>
...
...
@@ -175,7 +175,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"1. precondition"
sum=
"
fc02b5563aad2dbdf7d3d9058d13f62c
"
sum=
"
844fd2ef9205b3f4c098e9dd71e617b9
"
proved=
"true"
expanded=
"false"
shape=
"preconditionainfix >=V6c0Laprefix -V1Laprefix -V0Lainfix -V3c1Lado_moveV2V4Iainfix >=V3c1F"
>
...
...
@@ -235,7 +235,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"2. postcondition"
sum=
"
762aee9d06bb39d1023e5c19b8e3bcba
"
sum=
"
085f6aac34de83587f9f539445a78ebc
"
proved=
"true"
expanded=
"false"
shape=
"postconditioniiainfix <=V10V0ainfix >=V10V1ainfix <=V11aprefix -V1ainfix =V10aprefix -V11ainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V4ainfix -V3c1Laprefix -V9Iiiainfix >=V9V7ainfix <=V9V8ainfix <=aminmaxV5V6V8ainfix =V9aminmaxV5V6ainfix <aminmaxV5V6V7Aainfix <V8aminmaxV5V6FIainfix >=V6c0Laprefix -V1Laprefix -V0Lainfix -V3c1Lado_moveV2V4Iainfix >=V3c1F"
>
...
...
@@ -250,7 +250,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"1. postcondition"
sum=
"
db3f91a0a59f552158d7a7a1b3612828
"
sum=
"
896507065c99ea0ee97d8e13dd5e6019
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =V10aprefix -V11Iainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V4ainfix -V3c1Laprefix -V9Iiiainfix >=V9V7ainfix <=V9V8ainfix <=aminmaxV5V6V8ainfix =V9aminmaxV5V6ainfix <aminmaxV5V6V7Aainfix <V8aminmaxV5V6FIainfix >=V6c0Laprefix -V1Laprefix -V0Lainfix -V3c1Lado_moveV2V4Iainfix >=V3c1F"
>
...
...
@@ -270,7 +270,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"2. postcondition"
sum=
"
ee0d767f383db49077ea9b1cbe5a3181
"
sum=
"
b4035a89477ec6c3cc9f18677a311552
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix >=V10V1Iainfix <=V11aprefix -V1INainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V4ainfix -V3c1Laprefix -V9Iiiainfix >=V9V7ainfix <=V9V8ainfix <=aminmaxV5V6V8ainfix =V9aminmaxV5V6ainfix <aminmaxV5V6V7Aainfix <V8aminmaxV5V6FIainfix >=V6c0Laprefix -V1Laprefix -V0Lainfix -V3c1Lado_moveV2V4Iainfix >=V3c1F"
>
...
...
@@ -290,7 +290,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"109"
loccnumb=
"10"
loccnume=
"31"
expl=
"3. postcondition"
sum=
"
e995f931a6f654b51b82bb0ee88a642e
"
sum=
"
4483f965602c51f2bb7151bd18b692d1
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix <=V10V0INainfix <=V11aprefix -V1INainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V4ainfix -V3c1Laprefix -V9Iiiainfix >=V9V7ainfix <=V9V8ainfix <=aminmaxV5V6V8ainfix =V9aminmaxV5V6ainfix <aminmaxV5V6V7Aainfix <V8aminmaxV5V6FIainfix >=V6c0Laprefix -V1Laprefix -V0Lainfix -V3c1Lado_moveV2V4Iainfix >=V3c1F"
>
...
...
@@ -314,7 +314,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"VC for negabeta"
sum=
"
ffca5ea3e66e79f4b33682b603d00068
"
sum=
"
10b003198bf762bdc66fa147058ba6ad
"
proved=
"false"
expanded=
"true"
shape=
"iCiiainfix >=V4V1ainfix <=V4V0ainfix <=aminmaxV2V3V0ainfix =V4aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2aNiliiiainfix >=V9V1ainfix <=V9V0ainfix <=aminmaxV2V3V0ainfix =V9aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Iiiiainfix >=V9V1ainfix <=V9V8ainfix <=V11V8ainfix =V9V11ainfix <V11V1Aainfix <V8V11LaminaTuple2V2V3V10ainfix =V9V7ais_emptyV10LaelementsV6FAainfix >=V3c1LamaxV7V0iiainfix >=V7V1ainfix <=V7V0ainfix <=aminmaxV2V3V0ainfix =V7aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix >=V7V1Iiiainfix <=V7V0ainfix >=V7V1ainfix <=V12aprefix -V1ainfix =V7aprefix -V12ainfix <V12aprefix -V0Aainfix <aprefix -V1V12Laminmaxado_moveV2V5ainfix -V3c1FAainfix >=V3c1aConsVValegal_movesV2iiainfix >=V13V1ainfix <=V13V0ainfix <=aminmaxV2V3V0ainfix =V13aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2ainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -329,7 +329,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"1. postcondition"
sum=
"
f7ca4d3c20c4042ba2e1ed4718a03299
"
sum=
"
89e59e502c4e02f20fb7311ec0a088fe
"
proved=
"true"
expanded=
"false"
shape=
"postconditioniiainfix >=V4V1ainfix <=V4V0ainfix <=aminmaxV2V3V0ainfix =V4aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2Iainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -352,7 +352,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"1. postcondition"
sum=
"
14bc192e3ae00bd1a7b80a8504aae3b8
"
sum=
"
4164e1b94ff1bbc17d88e19ea42fcf4d
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix =V4aminmaxV2V3Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2Iainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -380,7 +380,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"2. postcondition"
sum=
"
3b1aac0f9ace3282f582b103139f7704
"
sum=
"
52040ad70852ccae8488ca23c44a88ad
"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix <=V4V0Iainfix <=aminmaxV2V3V0INainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2Iainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -408,7 +408,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"3. postcondition"
sum=
"
189a5206133eba38afac02b6253dcb7
4"
sum=
"
b3ae9d41235093b43f0fc1f072faa24
4"
proved=
"true"
expanded=
"false"
shape=
"postconditionainfix >=V4V1INainfix <=aminmaxV2V3V0INainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2Iainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -438,7 +438,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"2. postcondition"
sum=
"
afcde116ca7f2ded744a62399c9c6e90
"
sum=
"
65c667a48f56bcf053cd006a34e8c503
"
proved=
"true"
expanded=
"false"
shape=
"postconditionCiiainfix >=V4V1ainfix <=V4V0ainfix <=aminmaxV2V3V0ainfix =V4aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2aNiltaConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -453,7 +453,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"1. postcondition"
sum=
"
d7df61293877c9ac68b2a58e3827c0a5
"
sum=
"
c2100c185ec5bd38d60c9b6a2fd669bc
"
proved=
"true"
expanded=
"false"
shape=
"postconditionCainfix =V4aminmaxV2V3Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2aNiltaConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -489,7 +489,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"2. postcondition"
sum=
"
28a84ccab05e78a87ee3baf28a3014b4
"
sum=
"
75c132846ee7fc22be4b7c8e8ce2929e
"
proved=
"true"
expanded=
"false"
shape=
"postconditionCainfix <=V4V0Iainfix <=aminmaxV2V3V0INainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2aNiltaConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -525,7 +525,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"3. postcondition"
sum=
"
4b839296c81afd6587c0aaa462c0863f
"
sum=
"
f622ea7fc0c52c83e165c80090ef4904
"
proved=
"true"
expanded=
"false"
shape=
"postconditionCainfix >=V4V1INainfix <=aminmaxV2V3V0INainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Laposition_valueV2aNiltaConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -563,7 +563,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"3. precondition"
sum=
"
82bb910e4ca5d7c49ca3b6e1d7be88ac
"
sum=
"
aef005466f060aa69b73388674f7f361
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaNilainfix >=V3c1aConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -599,7 +599,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"4. postcondition"
sum=
"0
a2fe6dbcd49dd5e1a0df01bb03f650b
"
sum=
"0
dacec09eefcc86eff23a45f9da0ead4
"
proved=
"false"
expanded=
"true"
shape=
"postconditionCtaNiliiainfix >=V6V1ainfix <=V6V0ainfix <=aminmaxV2V3V0ainfix =V6aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Iainfix >=V6V1Iiiainfix <=V6V0ainfix >=V6V1ainfix <=V7aprefix -V1ainfix =V6aprefix -V7ainfix <V7aprefix -V0Aainfix <aprefix -V1V7Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1aConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -611,7 +611,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"5. precondition"
sum=
"
4d27c1bd77495733b7888ab6f4476fd9
"
sum=
"
2ff311f4242e2dd3d5c9641754c8c8e0
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaNilainfix >=V3c1LamaxV6V0INainfix >=V6V1Iiiainfix <=V6V0ainfix >=V6V1ainfix <=V8aprefix -V1ainfix =V6aprefix -V8ainfix <V8aprefix -V0Aainfix <aprefix -V1V8Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1aConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -647,7 +647,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"121"
loccnumb=
"7"
loccnume=
"15"
expl=
"6. postcondition"
sum=
"
4e1a92fdd2ad92a85a7ee66ae9e72668
"
sum=
"
9f5b4f07c5a0e7ab8ad80b406e8ca739
"
proved=
"false"
expanded=
"true"
shape=
"postconditionCtaNiliiainfix >=V8V1ainfix <=V8V0ainfix <=aminmaxV2V3V0ainfix =V8aminmaxV2V3ainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Iiiiainfix >=V8V1ainfix <=V8V7ainfix <=V10V7ainfix =V8V10ainfix <V10V1Aainfix <V7V10LaminaTuple2V2V3V9ainfix =V8V6ais_emptyV9LaelementsV5FIainfix >=V3c1LamaxV6V0INainfix >=V6V1Iiiainfix <=V6V0ainfix >=V6V1ainfix <=V11aprefix -V1ainfix =V6aprefix -V11ainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1aConsVValegal_movesV2INainfix =V3c0Iainfix >=V3c0F"
>
...
...
@@ -661,7 +661,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"VC for negabeta_rec"
sum=
"
d23f7bac344975e58ad81015254f9623
"
sum=
"
26c0dd6c3becae34d82fcf58ed5f776c
"
proved=
"false"
expanded=
"true"
shape=
"Ciiainfix >=V4V1ainfix <=V4V0ainfix <=V7V0ainfix =V4V7ainfix <V7V1Aainfix <V0V7LaminaTuple2V2V3V6INais_emptyV6LaelementsV5aNiliiiiainfix >=V13V1ainfix <=V13V0ainfix <=V15V0ainfix =V13V15ainfix <V15V1Aainfix <V0V15LaminaTuple2V2V3V14ainfix =V13V4ais_emptyV14LaelementsV5Iiiiainfix >=V13V1ainfix <=V13V12ainfix <=V17V12ainfix =V13V17ainfix <V17V1Aainfix <V12V17LaminaTuple2V2V3V16ainfix =V13V11ais_emptyV16LaelementsV9FAainfix >=V3c1LamaxV11V0iiiainfix >=V11V1ainfix <=V11V0ainfix <=V19V0ainfix =V11V19ainfix <V19V1Aainfix <V0V19LaminaTuple2V2V3V18ainfix =V11V4ais_emptyV18LaelementsV5ainfix >=V11V1LamaxV10V4Iiiainfix <=V10V0ainfix >=V10V1ainfix <=V20aprefix -V1ainfix =V10aprefix -V20ainfix <V20aprefix -V0Aainfix <aprefix -V1V20Laminmaxado_moveV2V8ainfix -V3c1FAainfix >=V3c1aConsVVV5Iainfix >=V3c1F"
>
...
...
@@ -676,7 +676,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"1. postcondition"
sum=
"
73aef1472406a280999a4fdbdd583468
"
sum=
"
e7d8dd92a3819de87e861df63c05371a
"
proved=
"true"
expanded=
"false"
shape=
"postconditionCiiainfix >=V4V1ainfix <=V4V0ainfix <=V7V0ainfix =V4V7ainfix <V7V1Aainfix <V0V7LaminaTuple2V2V3V6INais_emptyV6LaelementsV5aNiltaConsVVV5Iainfix >=V3c1F"
>
...
...
@@ -696,7 +696,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"2. precondition"
sum=
"
3ea1cf951a295a0438db8d797506dfae
"
sum=
"
8dfefa9409b3503d0b945636d6618466
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaNilainfix >=V3c1aConsVVV5Iainfix >=V3c1F"
>
...
...
@@ -716,7 +716,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"3. postcondition"
sum=
"
11f1f1c790e92f93845ac9609f82ec97
"
sum=
"
4efc4908328f6898158cbd0c734708e8
"
proved=
"false"
expanded=
"true"
shape=
"postconditionCtaNiliiiainfix >=V9V1ainfix <=V9V0ainfix <=V11V0ainfix =V9V11ainfix <V11V1Aainfix <V0V11LaminaTuple2V2V3V10ainfix =V9V4ais_emptyV10LaelementsV5Iainfix >=V9V1LamaxV8V4Iiiainfix <=V8V0ainfix >=V8V1ainfix <=V12aprefix -V1ainfix =V8aprefix -V12ainfix <V12aprefix -V0Aainfix <aprefix -V1V12Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1aConsVVV5Iainfix >=V3c1F"
>
...
...
@@ -728,7 +728,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"4. precondition"
sum=
"
9717d46d1a16d84331eac896ba258304
"
sum=
"
38e6e2bfb1000ba8db7a62873a22345a
"
proved=
"true"
expanded=
"false"
shape=
"preconditionCtaNilainfix >=V3c1LamaxV9V0INainfix >=V9V1LamaxV8V4Iiiainfix <=V8V0ainfix >=V8V1ainfix <=V11aprefix -V1ainfix =V8aprefix -V11ainfix <V11aprefix -V0Aainfix <aprefix -V1V11Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1aConsVVV5Iainfix >=V3c1F"
>
...
...
@@ -748,7 +748,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"139"
loccnumb=
"7"
loccnume=
"19"
expl=
"5. postcondition"
sum=
"
fd91d12fec269921cad9b0a022668e3b
"
sum=
"
89398fbaa9f239a49670bc10089323a6
"
proved=
"false"
expanded=
"true"
shape=
"postconditionCtaNiliiiainfix >=V11V1ainfix <=V11V0ainfix <=V13V0ainfix =V11V13ainfix <V13V1Aainfix <V0V13LaminaTuple2V2V3V12ainfix =V11V4ais_emptyV12LaelementsV5Iiiiainfix >=V11V1ainfix <=V11V10ainfix <=V15V10ainfix =V11V15ainfix <V15V1Aainfix <V10V15LaminaTuple2V2V3V14ainfix =V11V9ais_emptyV14LaelementsV7FIainfix >=V3c1LamaxV9V0INainfix >=V9V1LamaxV8V4Iiiainfix <=V8V0ainfix >=V8V1ainfix <=V16aprefix -V1ainfix =V8aprefix -V16ainfix <V16aprefix -V0Aainfix <aprefix -V1V16Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1aConsVVV5Iainfix >=V3c1F"
>
...
...
@@ -762,7 +762,7 @@
locfile=
"../alphaBeta.mlw"
loclnum=
"161"
loccnumb=
"4"
loccnume=
"14"
expl=
"VC for alpha_beta"
sum=
"
74aa737887ec0d637f394aee463c1610
"
sum=
"
58d1fe56c4bb9e80dd6a94c960150e0f
"
proved=
"true"
expanded=
"false"
shape=
"ainfix =V4aminmaxV0V1Iiiainfix >=V4V2ainfix <=V4V3ainfix <=aminmaxV0V1V3ainfix =V4aminmaxV0V1ainfix <aminmaxV0V1V2Aainfix <V3aminmaxV0V1FAainfix >=V1c0Laprefix -ainfinityLainfinityIainfix >=V1c0F"
>
...
...
examples/arm/why3session.xml
View file @
9bf1998f
...
...
@@ -24,7 +24,7 @@
locfile=
"../arm.mlw"
loclnum=
"16"
loccnumb=
"6"
loccnume=
"20"
expl=
"VC for insertion_sort"
sum=
"
5677a170e9f6faf600b34c4281eebd63
"
sum=
"
ff4534d299565274c09d1a7200c24c10
"
proved=
"false"
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"
>
...
...
@@ -50,7 +50,7 @@
locfile=
"../arm.mlw"
loclnum=
"120"
loccnumb=
"6"
loccnume=
"18"
expl=
"VC for path_init_l2"
sum=
"
19ae2913cea5458fb6929fc9f238efaf
"
sum=
"
a673c6b14e3f66097ab6521a75fc2975
"
proved=
"true"
expanded=
"true"
shape=
"ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F"
>
...
...
@@ -70,7 +70,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"0.
02
"
/>
<result
status=
"valid"
time=
"0.
14
"
/>
</proof>
</goal>
<goal
...
...
@@ -78,7 +78,7 @@
locfile=
"../arm.mlw"
loclnum=
"127"
loccnumb=
"6"
loccnume=
"18"
expl=
"VC for path_l2_exit"
sum=
"
bca45c9a7ef7fbe8792f11db8c6319ef
"
sum=
"
850b762a046fc7dd2686d4a5b7033244
"
proved=
"true"
expanded=
"true"
shape=
"ainfix =V0c9Iainfix =V4aFalseIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F"
>
...
...
examples/assigning_meanings_to_programs/why3session.xml
View file @
9bf1998f
...
...
@@ -24,7 +24,7 @@
locfile=
"../assigning_meanings_to_programs.mlw"
loclnum=
"12"
loccnumb=
"6"
loccnume=
"9"
expl=
"VC for sum"
sum=
"
17bf6dcb57a723007ce152bd4c333f35
"
sum=
"
e0ca4e8622864551ab60bb029148376f
"
proved=
"true"
expanded=
"true"
shape=
"iainfix =V3asumV2c1ainfix +V1c1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix <=V4V1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1Aainfix <=c0V0FF"
>
...
...
examples/bellman_ford/why3session.xml
View file @
9bf1998f
This diff is collapsed.
Click to expand it.
examples/binary_search/why3session.xml
View file @
9bf1998f
...
...
@@ -24,7 +24,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"17"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"5
8d7f9baa3142a5765eb3ebc3538afbb
"
sum=
"5
6a7828114cad28fdbf0f3086ba665f0
"
proved=
"true"
expanded=
"true"
shape=
"iNainfix =agetV2V5V1Iainfix <V5V0Aainfix <=c0V5Fiiainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -V6c1Fainfix >agetV2V6V1Aainfix <V6V0Aainfix <=c0V6ainfix <ainfix -V3V9ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V3Aainfix <=V9V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V9Iainfix =V9ainfix +V6c1Fainfix <agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Aainfix <=V6V3Aainfix <=V4V6Lainfix +V4adivainfix -V3V4c2ainfix <=V4V3Iainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FAainfix <=c0V0FF"
>
...
...
@@ -59,7 +59,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"60"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"
5954021440d95809176c18fd90076bd1
"
sum=
"
469d933c0ef6d53b10a8af8040766229
"
proved=
"true"
expanded=
"true"
shape=
"iNainfix =agetV2V5V1Iainfix <V5V0Aainfix <=c0V5Fiiainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -V6c1Fainfix >agetV2V6V1Aainfix <V6V0Aainfix <=c0V6ainfix <ainfix -V3V9ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V3Aainfix <=V9V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V9Iainfix =V9ainfix +V6c1Fainfix <agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Iainfix <=V6V3Aainfix <=V4V6FAainfix <=V4V3ainfix <=V4V3Iainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FAainfix <=c0V0FF"
>
...
...
@@ -86,7 +86,7 @@
locfile=
"../binary_search.mlw"
loclnum=
"100"
loccnumb=
"6"
loccnume=
"19"
expl=
"VC for binary_search"
sum=
"
c1b8b598df35a36bdae0936e15ba837
9"
sum=
"
b4024703c302726d0965763f55ca4a8
9"
proved=
"true"
expanded=
"true"
shape=
"iNainfix =agetV2V5V1Iainfix <V5V0Aainfix <=c0V5Fiiainfix =agetV2V7V1Aainfix <V7V0Aainfix <=c0V7ainfix <ainfix -V8V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V9V8Aainfix <=V4V9Iainfix =agetV2V9V1Iainfix <V9V0Aainfix <=c0V9FAainfix <V8V0Aainfix <=c0V4Iainfix =V8ainfix -V7c1FAainfix <=ainfix -V7c1amax_intAainfix <=amin_intainfix -V7c1ainfix >agetV2V7V1Aainfix <V7V0Aainfix <=c0V7ainfix <ainfix -V3V10ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V11V3Aainfix <=V10V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V10Iainfix =V10ainfix +V7c1FAainfix <=ainfix +V7c1amax_intAainfix <=amin_intainfix +V7c1ainfix <agetV2V7V1Aainfix <V7V0Aainfix <=c0V7Aainfix <=V7V3Aainfix <=V4V7Lainfix +V4V6Aainfix <=ainfix +V4V6amax_intAainfix <=amin_intainfix +V4V6Ladivainfix -V3V4c2Aainfix <=ainfix -V3V4amax_intAainfix <=amin_intainfix -V3V4ainfix <=V4V3Iainfix <=V12V3Aainfix <=V4V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <V3V0Aainfix <=c0V4FAainfix <=V13ainfix -V0c1Aainfix <=c0V13Iainfix =agetV2V13V1Iainfix <V13V0Aainfix <=c0V13FAainfix <ainfix -V0c1V0Aainfix <=c0c0Aainfix <=ainfix -V0c1amax_intAainfix <=amin_intainfix -V0c1Iainfix <=agetV2V14agetV2V15Iainfix <V15V0Aainfix <=V14V15Aainfix <=c0V14FAainfix <=V0amax_intAainfix <=c0V0FF"
>
...
...
examples/bitvectors/bitvector/why3session.xml
View file @
9bf1998f
...
...
@@ -16,7 +16,7 @@
<prover
id=
"3"
name=
"CVC4"
version=
"1.
0
"
/>
version=
"1.
2
"
/>
<prover
id=
"4"
name=
"Coq"
...
...
@@ -200,7 +200,7 @@
edited=
"bitvector_BitVector_to_nat_of_zero_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"1.
65
"
/>
<result
status=
"valid"
time=
"1.
23
"
/>
</proof>
</goal>
<goal
...
...
@@ -218,7 +218,7 @@
edited=
"bitvector_BitVector_to_nat_of_one_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"
2.32
"
/>
<result
status=
"valid"
time=
"
1.31
"
/>
</proof>
</goal>
<goal
...
...
@@ -236,7 +236,7 @@
edited=
"bitvector_BitVector_to_nat_sub_footprint_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"valid"
time=
"
8
.33"
/>
<result
status=
"valid"
time=
"
9
.33"
/>
</proof>
</goal>
<goal
...
...
@@ -529,7 +529,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5
.04"
/>
<result
status=
"
valid"
time=
"0
.04"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -1756,7 +1756,7 @@
locfile=
"../bitvector.why"
loclnum=
"455"
loccnumb=
"7"
loccnume=
"24"
sum=
"d3a213e5d10a94f1672c2f81616ef199"
proved=
"
fals
e"
proved=
"
tru
e"
expanded=
"true"
shape=
"ainfix =ato_natalsrabvonec18c16383"
>
<proof
...
...
@@ -1789,7 +1789,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5.08
"
/>
<result
status=
"
valid"
time=
"4.26
"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -1821,7 +1821,7 @@
locfile=
"../bitvector.why"
loclnum=
"458"
loccnumb=
"7"
loccnume=
"24"
sum=
"89780e352ce90762edd80b151dd0fa63"
proved=
"
fals
e"
proved=
"
tru
e"
expanded=
"true"
shape=
"ainfix =ato_natalsrabvonec17c32767"
>
<proof
...
...
@@ -1854,7 +1854,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5.06
"
/>
<result
status=
"
valid"
time=
"3.72
"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -1886,7 +1886,7 @@
locfile=
"../bitvector.why"
loclnum=
"461"
loccnumb=
"7"
loccnume=
"24"
sum=
"7cf453c2e02082e54109f72a5e101fef"
proved=
"
fals
e"
proved=
"
tru
e"
expanded=
"true"
shape=
"ainfix =ato_natalsrabvonec16c65535"
>
<proof
...
...
@@ -1919,7 +1919,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5.06
"
/>
<result
status=
"
valid"
time=
"3.12
"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -1951,7 +1951,7 @@
locfile=
"../bitvector.why"
loclnum=
"469"
loccnumb=
"7"
loccnume=
"24"
sum=
"81a4492651176e01d54e30bb34905b03"
proved=
"
fals
e"
proved=
"
tru
e"
expanded=
"true"
shape=
"ainfix =ato_natalsrabvonec15c131071"
>
<proof
...
...
@@ -1984,7 +1984,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5.03
"
/>
<result
status=
"
valid"
time=
"2.48
"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -2016,7 +2016,7 @@
locfile=
"../bitvector.why"
loclnum=
"472"
loccnumb=
"7"
loccnume=
"24"
sum=
"24edb5c87fb553582f0a0fa7d1d0ba98"
proved=
"
fals
e"
proved=
"
tru
e"
expanded=
"true"
shape=
"ainfix =ato_natalsrabvonec14c262143"
>
<proof
...
...
@@ -2049,7 +2049,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5.03
"
/>
<result
status=
"
valid"
time=
"1.85
"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -2081,7 +2081,7 @@
locfile=
"../bitvector.why"
loclnum=
"475"
loccnumb=
"7"
loccnume=
"24"
sum=
"843cbb41fe2fcc3af6648d1f99201031"
proved=
"
fals
e"
proved=
"
tru
e"
expanded=
"true"
shape=
"ainfix =ato_natalsrabvonec13c524287"
>
<proof
...
...
@@ -2114,7 +2114,7 @@
memlimit=
"1000"
obsolete=
"false"
archived=
"false"
>
<result
status=
"
timeout"
time=
"5.03
"
/>
<result
status=
"
valid"
time=
"1.50
"
/>
</proof>
<proof
prover=
"5"
...
...
@@ -2146,7 +2146,7 @@
locfile=
"../bitvector.why"