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
121
Issues
121
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
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
8e560e42
Commit
8e560e42
authored
May 14, 2018
by
MARCHE Claude
1
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
removed deprecated transformations split_*_wp
parent
4725ff4c
Changes
225
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
225 changed files
with
2114 additions
and
2129 deletions
+2114
-2129
bench/ce/jlamp0/why3session.xml
bench/ce/jlamp0/why3session.xml
+2
-2
examples/WP_revisited/blocking_semantics5/why3session.xml
examples/WP_revisited/blocking_semantics5/why3session.xml
+10
-10
examples/WP_revisited/wp2/why3session.xml
examples/WP_revisited/wp2/why3session.xml
+2
-2
examples/algo63/why3session.xml
examples/algo63/why3session.xml
+2
-2
examples/algo64/why3session.xml
examples/algo64/why3session.xml
+2
-2
examples/algo65/why3session.xml
examples/algo65/why3session.xml
+3
-3
examples/all_distinct/why3session.xml
examples/all_distinct/why3session.xml
+1
-1
examples/arm/why3session.xml
examples/arm/why3session.xml
+1
-1
examples/avl/association_list/why3session.xml
examples/avl/association_list/why3session.xml
+6
-6
examples/avl/avl/why3session.xml
examples/avl/avl/why3session.xml
+4
-4
examples/avl/priority_queue/why3session.xml
examples/avl/priority_queue/why3session.xml
+15
-15
examples/avl/ral/why3session.xml
examples/avl/ral/why3session.xml
+3
-3
examples/avl/sorted/why3session.xml
examples/avl/sorted/why3session.xml
+1
-1
examples/avl/tables/why3session.xml
examples/avl/tables/why3session.xml
+20
-20
examples/bag/why3session.xml
examples/bag/why3session.xml
+2
-2
examples/balance/why3session.xml
examples/balance/why3session.xml
+1
-1
examples/bellman_ford/why3session.xml
examples/bellman_ford/why3session.xml
+13
-13
examples/bignum/why3session.xml
examples/bignum/why3session.xml
+4
-4
examples/binary_search/why3session.xml
examples/binary_search/why3session.xml
+1
-1
examples/binary_sort/why3session.xml
examples/binary_sort/why3session.xml
+2
-2
examples/binary_sqrt/why3session.xml
examples/binary_sqrt/why3session.xml
+2
-2
examples/binomial_heap/why3session.xml
examples/binomial_heap/why3session.xml
+13
-13
examples/bitcount/why3session.xml
examples/bitcount/why3session.xml
+31
-31
examples/bitvector_examples/why3session.xml
examples/bitvector_examples/why3session.xml
+1
-1
examples/bitwalker/why3session.xml
examples/bitwalker/why3session.xml
+14
-14
examples/braun_trees/why3session.xml
examples/braun_trees/why3session.xml
+8
-8
examples/bresenham/why3session.xml
examples/bresenham/why3session.xml
+1
-1
examples/bubble_sort/why3session.xml
examples/bubble_sort/why3session.xml
+1
-1
examples/checking_a_large_routine/why3session.xml
examples/checking_a_large_routine/why3session.xml
+2
-2
examples/coincidence_count/why3session.xml
examples/coincidence_count/why3session.xml
+1
-1
examples/coincidence_count_list/why3session.xml
examples/coincidence_count_list/why3session.xml
+2
-2
examples/conjugate/why3session.xml
examples/conjugate/why3session.xml
+1
-1
examples/counting_sort/why3session.xml
examples/counting_sort/why3session.xml
+3
-3
examples/cubic_root/why3session.xml
examples/cubic_root/why3session.xml
+1
-1
examples/cursor/why3session.xml
examples/cursor/why3session.xml
+5
-5
examples/decrease1/why3session.xml
examples/decrease1/why3session.xml
+2
-2
examples/defunctionalization/why3session.xml
examples/defunctionalization/why3session.xml
+9
-9
examples/dfa_example/why3session.xml
examples/dfa_example/why3session.xml
+6
-6
examples/dfs/why3session.xml
examples/dfs/why3session.xml
+2
-2
examples/dijkstra/why3session.xml
examples/dijkstra/why3session.xml
+2
-2
examples/division/why3session.xml
examples/division/why3session.xml
+1
-1
examples/double_wp/compiler/why3session.xml
examples/double_wp/compiler/why3session.xml
+31
-31
examples/double_wp/logic/why3session.xml
examples/double_wp/logic/why3session.xml
+6
-6
examples/double_wp/specs/why3session.xml
examples/double_wp/specs/why3session.xml
+9
-9
examples/dyck/why3session.xml
examples/dyck/why3session.xml
+6
-6
examples/edit_distance/why3session.xml
examples/edit_distance/why3session.xml
+4
-4
examples/esterel/why3session.xml
examples/esterel/why3session.xml
+3
-3
examples/euler002/why3session.xml
examples/euler002/why3session.xml
+2
-2
examples/euler011/why3session.xml
examples/euler011/why3session.xml
+98
-98
examples/fenwick/why3session.xml
examples/fenwick/why3session.xml
+1
-1
examples/fib_memo/why3session.xml
examples/fib_memo/why3session.xml
+1
-1
examples/fibonacci/why3session.xml
examples/fibonacci/why3session.xml
+10
-10
examples/find/why3session.xml
examples/find/why3session.xml
+5
-5
examples/finger_trees/why3session.xml
examples/finger_trees/why3session.xml
+3
-3
examples/flag/why3session.xml
examples/flag/why3session.xml
+1
-1
examples/flag2/why3session.xml
examples/flag2/why3session.xml
+2
-2
examples/foveoos11_challenge1/why3session.xml
examples/foveoos11_challenge1/why3session.xml
+1
-1
examples/foveoos11_challenge3/why3session.xml
examples/foveoos11_challenge3/why3session.xml
+2
-2
examples/gcd/why3session.xml
examples/gcd/why3session.xml
+4
-4
examples/gcd_bezout/why3session.xml
examples/gcd_bezout/why3session.xml
+1
-1
examples/generate_all_trees/why3session.xml
examples/generate_all_trees/why3session.xml
+6
-6
examples/hackers-delight/why3session.xml
examples/hackers-delight/why3session.xml
+5
-5
examples/hashtbl_impl/why3session.xml
examples/hashtbl_impl/why3session.xml
+7
-7
examples/in_progress/2wp_gen/base/why3session.xml
examples/in_progress/2wp_gen/base/why3session.xml
+2
-2
examples/in_progress/2wp_gen/game/why3session.xml
examples/in_progress/2wp_gen/game/why3session.xml
+118
-118
examples/in_progress/2wp_gen/game_fmla/why3session.xml
examples/in_progress/2wp_gen/game_fmla/why3session.xml
+89
-89
examples/in_progress/2wp_gen/game_wp/why3session.xml
examples/in_progress/2wp_gen/game_wp/why3session.xml
+58
-58
examples/in_progress/2wp_gen/order/why3session.xml
examples/in_progress/2wp_gen/order/why3session.xml
+16
-16
examples/in_progress/2wp_gen/transfinite/why3session.xml
examples/in_progress/2wp_gen/transfinite/why3session.xml
+10
-10
examples/in_progress/2wp_gen/transition/why3session.xml
examples/in_progress/2wp_gen/transition/why3session.xml
+29
-29
examples/in_progress/2wp_gen/zorn/why3session.xml
examples/in_progress/2wp_gen/zorn/why3session.xml
+5
-5
examples/in_progress/alphaBeta/why3session.xml
examples/in_progress/alphaBeta/why3session.xml
+6
-6
examples/in_progress/avl/association_list/why3session.xml
examples/in_progress/avl/association_list/why3session.xml
+8
-8
examples/in_progress/avl/avl/why3session.xml
examples/in_progress/avl/avl/why3session.xml
+20
-20
examples/in_progress/avl/map/why3session.xml
examples/in_progress/avl/map/why3session.xml
+107
-107
examples/in_progress/avl/monoid/association_list/why3session.xml
...s/in_progress/avl/monoid/association_list/why3session.xml
+8
-8
examples/in_progress/avl/monoid/avl/why3session.xml
examples/in_progress/avl/monoid/avl/why3session.xml
+5
-5
examples/in_progress/avl/monoid/map/why3session.xml
examples/in_progress/avl/monoid/map/why3session.xml
+34
-34
examples/in_progress/avl/monoid/priority_queue/why3session.xml
...les/in_progress/avl/monoid/priority_queue/why3session.xml
+15
-15
examples/in_progress/avl/monoid/ral/why3session.xml
examples/in_progress/avl/monoid/ral/why3session.xml
+3
-3
examples/in_progress/avl/monoid/sorted/why3session.xml
examples/in_progress/avl/monoid/sorted/why3session.xml
+1
-1
examples/in_progress/avl/ral/why3session.xml
examples/in_progress/avl/ral/why3session.xml
+5
-5
examples/in_progress/avl/sorted/why3session.xml
examples/in_progress/avl/sorted/why3session.xml
+3
-3
examples/in_progress/avl_generic_dev/association_list/why3session.xml
...progress/avl_generic_dev/association_list/why3session.xml
+3
-3
examples/in_progress/avl_generic_dev/avl/why3session.xml
examples/in_progress/avl_generic_dev/avl/why3session.xml
+20
-20
examples/in_progress/avl_generic_dev/sorted/why3session.xml
examples/in_progress/avl_generic_dev/sorted/why3session.xml
+2
-2
examples/in_progress/bigInt/why3session.xml
examples/in_progress/bigInt/why3session.xml
+12
-12
examples/in_progress/cek/why3session.xml
examples/in_progress/cek/why3session.xml
+4
-4
examples/in_progress/convex_hull/why3session.xml
examples/in_progress/convex_hull/why3session.xml
+2
-2
examples/in_progress/hamming_sequence/why3session.xml
examples/in_progress/hamming_sequence/why3session.xml
+2
-2
examples/in_progress/koda_ruskey/why3session.xml
examples/in_progress/koda_ruskey/why3session.xml
+36
-36
examples/in_progress/mini-compiler-backward/compiler/why3session.xml
..._progress/mini-compiler-backward/compiler/why3session.xml
+27
-27
examples/in_progress/mini-compiler-backward/logic/why3session.xml
.../in_progress/mini-compiler-backward/logic/why3session.xml
+5
-5
examples/in_progress/mini-compiler-backward/specs/why3session.xml
.../in_progress/mini-compiler-backward/specs/why3session.xml
+12
-12
examples/in_progress/mini-compiler-backward/vm/why3session.xml
...les/in_progress/mini-compiler-backward/vm/why3session.xml
+3
-3
examples/in_progress/mp/why3session.xml
examples/in_progress/mp/why3session.xml
+24
-24
examples/in_progress/my_cosine/why3session.xml
examples/in_progress/my_cosine/why3session.xml
+3
-3
examples/in_progress/my_exp/why3session.xml
examples/in_progress/my_exp/why3session.xml
+1
-1
examples/in_progress/next_digit_sum/why3session.xml
examples/in_progress/next_digit_sum/why3session.xml
+4
-4
examples/in_progress/simple_priority_queue/why3session.xml
examples/in_progress/simple_priority_queue/why3session.xml
+4
-4
examples/in_progress/simple_queue/why3session.xml
examples/in_progress/simple_queue/why3session.xml
+1
-1
examples/in_progress/sudoku_reloaded/why3session.xml
examples/in_progress/sudoku_reloaded/why3session.xml
+9
-9
examples/in_progress/why3_logic/logic_semantic/why3session.xml
...les/in_progress/why3_logic/logic_semantic/why3session.xml
+35
-35
examples/in_progress/why3_logic/logic_syntax/why3session.xml
examples/in_progress/why3_logic/logic_syntax/why3session.xml
+31
-31
examples/in_progress/why3_logic/logic_typing/why3session.xml
examples/in_progress/why3_logic/logic_typing/why3session.xml
+30
-30
examples/in_progress/why3_logic/support/why3session.xml
examples/in_progress/why3_logic/support/why3session.xml
+24
-24
examples/in_progress/why3_logic/term/why3session.xml
examples/in_progress/why3_logic/term/why3session.xml
+2
-2
examples/in_progress/why3_logic/ty/why3session.xml
examples/in_progress/why3_logic/ty/why3session.xml
+1
-1
examples/insertion_sort/why3session.xml
examples/insertion_sort/why3session.xml
+2
-2
examples/insertion_sort_list/why3session.xml
examples/insertion_sort_list/why3session.xml
+2
-2
examples/insertion_sort_naive/why3session.xml
examples/insertion_sort_naive/why3session.xml
+4
-4
examples/inverse_in_place/why3session.xml
examples/inverse_in_place/why3session.xml
+5
-5
examples/isqrt/why3session.xml
examples/isqrt/why3session.xml
+4
-4
examples/isqrt_von_neumann/why3session.xml
examples/isqrt_von_neumann/why3session.xml
+7
-7
examples/kmp/why3session.xml
examples/kmp/why3session.xml
+4
-4
examples/knuth_prime_numbers/why3session.xml
examples/knuth_prime_numbers/why3session.xml
+7
-7
examples/koda_ruskey/why3session.xml
examples/koda_ruskey/why3session.xml
+25
-25
examples/largest_prime_factor/why3session.xml
examples/largest_prime_factor/why3session.xml
+7
-7
examples/lcp/why3session.xml
examples/lcp/why3session.xml
+1
-1
examples/leftist_heap/why3session.xml
examples/leftist_heap/why3session.xml
+1
-1
examples/linear_probing/why3session.xml
examples/linear_probing/why3session.xml
+32
-32
examples/linked_list_rev/why3session.xml
examples/linked_list_rev/why3session.xml
+15
-15
examples/logic/hello_proof/why3session.xml
examples/logic/hello_proof/why3session.xml
+1
-1
examples/max_matrix/why3session.xml
examples/max_matrix/why3session.xml
+7
-7
examples/maximum_subarray/why3session.xml
examples/maximum_subarray/why3session.xml
+13
-13
examples/mccarthy/why3session.xml
examples/mccarthy/why3session.xml
+1
-1
examples/mergesort_array/why3session.xml
examples/mergesort_array/why3session.xml
+16
-16
examples/mergesort_list/why3session.xml
examples/mergesort_list/why3session.xml
+15
-15
examples/mergesort_queue/why3session.xml
examples/mergesort_queue/why3session.xml
+3
-3
examples/mjrty/why3session.xml
examples/mjrty/why3session.xml
+1
-1
examples/muller/why3session.xml
examples/muller/why3session.xml
+1
-1
examples/my_cosine/why3session.xml
examples/my_cosine/why3session.xml
+1
-1
examples/optimal_replay/why3session.xml
examples/optimal_replay/why3session.xml
+2
-2
examples/patience/why3session.xml
examples/patience/why3session.xml
+8
-8
examples/pigeonhole/why3session.xml
examples/pigeonhole/why3session.xml
+1
-1
examples/power/why3session.xml
examples/power/why3session.xml
+3
-3
examples/prover/BacktrackArray/why3session.xml
examples/prover/BacktrackArray/why3session.xml
+11
-11
examples/prover/Firstorder_formula_impl/why3session.xml
examples/prover/Firstorder_formula_impl/why3session.xml
+43
-43
examples/prover/Firstorder_formula_list_impl/why3session.xml
examples/prover/Firstorder_formula_list_impl/why3session.xml
+19
-19
examples/prover/Firstorder_formula_list_spec/why3session.xml
examples/prover/Firstorder_formula_list_spec/why3session.xml
+4
-4
examples/prover/Firstorder_formula_spec/why3session.xml
examples/prover/Firstorder_formula_spec/why3session.xml
+16
-16
examples/prover/Firstorder_semantics/why3session.xml
examples/prover/Firstorder_semantics/why3session.xml
+7
-7
examples/prover/Firstorder_symbol_impl/why3session.xml
examples/prover/Firstorder_symbol_impl/why3session.xml
+5
-5
examples/prover/Firstorder_symbol_spec/why3session.xml
examples/prover/Firstorder_symbol_spec/why3session.xml
+1
-1
examples/prover/Firstorder_tableau_impl/why3session.xml
examples/prover/Firstorder_tableau_impl/why3session.xml
+10
-10
examples/prover/Firstorder_tableau_spec/why3session.xml
examples/prover/Firstorder_tableau_spec/why3session.xml
+5
-5
examples/prover/Firstorder_term_impl/why3session.xml
examples/prover/Firstorder_term_impl/why3session.xml
+37
-37
examples/prover/Firstorder_term_spec/why3session.xml
examples/prover/Firstorder_term_spec/why3session.xml
+12
-12
examples/prover/FormulaTransformations/why3session.xml
examples/prover/FormulaTransformations/why3session.xml
+72
-72
examples/prover/ISet/why3session.xml
examples/prover/ISet/why3session.xml
+4
-4
examples/prover/Prover/why3session.xml
examples/prover/Prover/why3session.xml
+60
-60
examples/prover/ProverMain/why3session.xml
examples/prover/ProverMain/why3session.xml
+3
-3
examples/prover/Unification/why3session.xml
examples/prover/Unification/why3session.xml
+34
-34
examples/queens/why3session.xml
examples/queens/why3session.xml
+8
-8
examples/queens_bv/why3session.xml
examples/queens_bv/why3session.xml
+11
-11
examples/quicksort/why3session.xml
examples/quicksort/why3session.xml
+6
-6
examples/random_access_list/why3session.xml
examples/random_access_list/why3session.xml
+8
-8
examples/register_allocation/why3session.xml
examples/register_allocation/why3session.xml
+5
-5
examples/relabel/why3session.xml
examples/relabel/why3session.xml
+1
-1
examples/remove_duplicate/why3session.xml
examples/remove_duplicate/why3session.xml
+1
-1
examples/remove_duplicate_hash/why3session.xml
examples/remove_duplicate_hash/why3session.xml
+2
-2
examples/residual/why3session.xml
examples/residual/why3session.xml
+5
-5
examples/rightmostbittrick/why3session.xml
examples/rightmostbittrick/why3session.xml
+2
-2
examples/ropes/why3session.xml
examples/ropes/why3session.xml
+12
-12
examples/same_fringe/why3session.xml
examples/same_fringe/why3session.xml
+2
-2
examples/schorr_waite/why3session.xml
examples/schorr_waite/why3session.xml
+15
-15
examples/schorr_waite_via_recursion/why3session.xml
examples/schorr_waite_via_recursion/why3session.xml
+1
-1
examples/selection_sort/why3session.xml
examples/selection_sort/why3session.xml
+3
-3
examples/sf/why3session.xml
examples/sf/why3session.xml
+3
-3
examples/sieve/why3session.xml
examples/sieve/why3session.xml
+6
-6
examples/skew_heaps/why3session.xml
examples/skew_heaps/why3session.xml
+6
-6
examples/snapshotable_trees/why3session.xml
examples/snapshotable_trees/why3session.xml
+4
-4
examples/stdlib/array/why3session.xml
examples/stdlib/array/why3session.xml
+2
-2
examples/stdlib/list/why3session.xml
examples/stdlib/list/why3session.xml
+9
-9
examples/sudoku/why3session.xml
examples/sudoku/why3session.xml
+3
-3
examples/sum_of_digits/why3session.xml
examples/sum_of_digits/why3session.xml
+2
-2
examples/sumrange/why3session.xml
examples/sumrange/why3session.xml
+4
-4
examples/tests-provers/ieee_float/why3session.xml
examples/tests-provers/ieee_float/why3session.xml
+3
-3
examples/tests/bv-smtlib-realization/why3session.xml
examples/tests/bv-smtlib-realization/why3session.xml
+1
-1
examples/there_and_back_again/why3session.xml
examples/there_and_back_again/why3session.xml
+4
-4
examples/topological_sorting/why3session.xml
examples/topological_sorting/why3session.xml
+7
-7
examples/tortoise_and_hare/why3session.xml
examples/tortoise_and_hare/why3session.xml
+1
-1
examples/tower_of_hanoi/why3session.xml
examples/tower_of_hanoi/why3session.xml
+3
-3
examples/toy_compiler/why3session.xml
examples/toy_compiler/why3session.xml
+1
-1
examples/tree_height/why3session.xml
examples/tree_height/why3session.xml
+2
-2
examples/tree_of_array/why3session.xml
examples/tree_of_array/why3session.xml
+2
-2
examples/tree_of_list/why3session.xml
examples/tree_of_list/why3session.xml
+2
-2
examples/unraveling_a_card_trick/why3session.xml
examples/unraveling_a_card_trick/why3session.xml
+5
-5
examples/vacid_0_binary_heaps/proofs/why3session.xml
examples/vacid_0_binary_heaps/proofs/why3session.xml
+21
-21
examples/vacid_0_build_maze/why3session.xml
examples/vacid_0_build_maze/why3session.xml
+3
-3
examples/vacid_0_red_black_trees/why3session.xml
examples/vacid_0_red_black_trees/why3session.xml
+18
-18
examples/vacid_0_sparse_array/why3session.xml
examples/vacid_0_sparse_array/why3session.xml
+2
-2
examples/verifythis_2015_dancing_links/why3session.xml
examples/verifythis_2015_dancing_links/why3session.xml
+2
-2
examples/verifythis_2015_parallel_gcd/why3session.xml
examples/verifythis_2015_parallel_gcd/why3session.xml
+3
-3
examples/verifythis_2015_relaxed_prefix/why3session.xml
examples/verifythis_2015_relaxed_prefix/why3session.xml
+1
-1
examples/verifythis_2016_matrix_multiplication/matrices/why3session.xml
...ythis_2016_matrix_multiplication/matrices/why3session.xml
+13
-13
examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3session.xml
..._matrix_multiplication/matrices_ring_simp/why3session.xml
+4
-4
examples/verifythis_2016_matrix_multiplication/naive/why3session.xml
...rifythis_2016_matrix_multiplication/naive/why3session.xml
+1
-1
examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
...ythis_2016_matrix_multiplication/strassen/why3session.xml
+5
-5
examples/verifythis_2016_matrix_multiplication/sum_extended/why3session.xml
...s_2016_matrix_multiplication/sum_extended/why3session.xml
+2
-2
examples/verifythis_2016_tree_traversal/why3session.xml
examples/verifythis_2016_tree_traversal/why3session.xml
+5
-5
examples/verifythis_PrefixSumRec/why3session.xml
examples/verifythis_PrefixSumRec/why3session.xml
+6
-6
examples/verifythis_fm2012_LRS/why3session.xml
examples/verifythis_fm2012_LRS/why3session.xml
+6
-6
examples/verifythis_fm2012_treedel/why3session.xml
examples/verifythis_fm2012_treedel/why3session.xml
+3
-3
examples/vstte10_aqueue/why3session.xml
examples/vstte10_aqueue/why3session.xml
+1
-1
examples/vstte10_inverting/why3session.xml
examples/vstte10_inverting/why3session.xml
+5
-5
examples/vstte10_max_sum/why3session.xml
examples/vstte10_max_sum/why3session.xml
+5
-5
examples/vstte10_queens/why3session.xml
examples/vstte10_queens/why3session.xml
+1
-1
examples/vstte10_search_list/why3session.xml
examples/vstte10_search_list/why3session.xml
+2
-2
examples/vstte12_bfs/why3session.xml
examples/vstte12_bfs/why3session.xml
+10
-10
examples/vstte12_combinators/why3session.xml
examples/vstte12_combinators/why3session.xml
+12
-12
examples/vstte12_ring_buffer/why3session.xml
examples/vstte12_ring_buffer/why3session.xml
+13
-13
examples/vstte12_tree_reconstruction/why3session.xml
examples/vstte12_tree_reconstruction/why3session.xml
+7
-7
examples/vstte12_two_way_sort/why3session.xml
examples/vstte12_two_way_sort/why3session.xml
+2
-2
examples/warshall_algorithm/why3session.xml
examples/warshall_algorithm/why3session.xml
+6
-6
examples/zeros/why3session.xml
examples/zeros/why3session.xml
+2
-2
src/transform/split_goal.ml
src/transform/split_goal.ml
+0
-10
src/transform/split_goal.mli
src/transform/split_goal.mli
+2
-7
tests/demo-itp/why3session.xml
tests/demo-itp/why3session.xml
+2
-2
tests/example-add/why3session.xml
tests/example-add/why3session.xml
+3
-3
tests/label/why3session.xml
tests/label/why3session.xml
+2
-2
tests/test_itp/why3session.xml
tests/test_itp/why3session.xml
+1
-1
tests/test_merge/why3session.xml
tests/test_merge/why3session.xml
+1
-1
tests/theory-sessions/bintree/why3session.xml
tests/theory-sessions/bintree/why3session.xml
+2
-2
tests/theory-sessions/hashtbl/why3session.xml
tests/theory-sessions/hashtbl/why3session.xml
+6
-6
No files found.
bench/ce/jlamp0/why3session.xml
View file @
8e560e42
...
...
@@ -6,7 +6,7 @@
<file
name=
"../jlamp0.mlw"
>
<theory
name=
"M"
>
<goal
name=
"WP_parameter p1"
expl=
"VC for p1"
>
<transf
name=
"split_
intros_goal_wp
"
>
<transf
name=
"split_
vc
"
>
<goal
name=
"WP_parameter p1.0"
expl=
"assertion"
>
<proof
prover=
"0"
><result
status=
"unknown"
time=
"0.01"
/></proof>
</goal>
...
...
@@ -19,7 +19,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter p2"
expl=
"VC for p2"
>
<transf
name=
"split_
intros_goal_wp
"
>
<transf
name=
"split_
vc
"
>
<goal
name=
"WP_parameter p2.0"
expl=
"loop invariant init"
>
<proof
prover=
"0"
><result
status=
"unknown"
time=
"0.00"
/></proof>
</goal>
...
...
examples/WP_revisited/blocking_semantics5/why3session.xml
View file @
8e560e42
...
...
@@ -76,7 +76,7 @@
<goal
name=
"eval_type_term"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_type_term.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_type_term.1.1"
expl=
""
>
<proof
prover=
"3"
timelimit=
"5"
><result
status=
"valid"
time=
"0.06"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.07"
steps=
"131"
/></proof>
...
...
@@ -110,7 +110,7 @@
<goal
name=
"eval_msubst_term"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_msubst_term.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_msubst_term.1.1"
expl=
""
>
<proof
prover=
"3"
timelimit=
"5"
memlimit=
"4000"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.04"
steps=
"14"
/></proof>
...
...
@@ -134,7 +134,7 @@
<goal
name=
"eval_msubst"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_msubst.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_msubst.1.1"
expl=
""
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.10"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.05"
steps=
"34"
/></proof>
...
...
@@ -183,7 +183,7 @@
<goal
name=
"eval_swap_term"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_swap_term.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_swap_term.1.1"
expl=
""
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.08"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.04"
steps=
"12"
/></proof>
...
...
@@ -206,7 +206,7 @@
<goal
name=
"eval_swap_gen"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_swap_gen.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_swap_gen.1.1"
expl=
""
>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.03"
steps=
"47"
/></proof>
<proof
prover=
"10"
><result
status=
"valid"
time=
"0.04"
/></proof>
...
...
@@ -261,7 +261,7 @@
<goal
name=
"eval_term_change_free"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_term_change_free.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_term_change_free.1.1"
expl=
""
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.04"
steps=
"7"
/></proof>
...
...
@@ -285,7 +285,7 @@
<goal
name=
"eval_change_free"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"eval_change_free.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"eval_change_free.1.1"
expl=
""
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.06"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.05"
steps=
"35"
/></proof>
...
...
@@ -371,7 +371,7 @@
<goal
name=
"monotonicity"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"monotonicity.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"monotonicity.1.1"
expl=
""
>
<proof
prover=
"3"
timelimit=
"5"
><result
status=
"valid"
time=
"0.08"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.09"
/></proof>
...
...
@@ -401,7 +401,7 @@
<goal
name=
"distrib_conj"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"distrib_conj.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"distrib_conj.1.1"
expl=
""
>
<proof
prover=
"3"
timelimit=
"5"
><result
status=
"valid"
time=
"0.07"
/></proof>
<proof
prover=
"9"
><result
status=
"valid"
time=
"0.06"
steps=
"30"
/></proof>
...
...
@@ -433,7 +433,7 @@
<goal
name=
"progress"
expl=
""
>
<transf
name=
"induction_ty_lex"
>
<goal
name=
"progress.1"
expl=
""
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"progress.1.1"
expl=
""
>
<proof
prover=
"3"
timelimit=
"5"
><result
status=
"valid"
time=
"0.06"
/></proof>
<proof
prover=
"7"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
examples/WP_revisited/wp2/why3session.xml
View file @
8e560e42
...
...
@@ -102,7 +102,7 @@
<proof
prover=
"7"
timelimit=
"3"
memlimit=
"0"
><result
status=
"valid"
time=
"0.02"
steps=
"8"
/></proof>
</goal>
<goal
name=
"WP_parameter compute_writes"
expl=
"VC for compute_writes"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter compute_writes.1"
expl=
"postcondition"
>
<proof
prover=
"7"
timelimit=
"3"
memlimit=
"0"
><result
status=
"valid"
time=
"0.06"
steps=
"94"
/></proof>
</goal>
...
...
@@ -139,7 +139,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter wp"
expl=
"VC for wp"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter wp.1"
expl=
"postcondition"
>
<proof
prover=
"2"
timelimit=
"3"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.00"
/></proof>
...
...
examples/algo63/why3session.xml
View file @
8e560e42
...
...
@@ -10,7 +10,7 @@
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.05"
steps=
"29"
/></proof>
</goal>
<goal
name=
"WP_parameter partition_"
expl=
"VC for partition_"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter partition_.0"
expl=
"index in array bounds"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"6"
/></proof>
</goal>
...
...
@@ -476,7 +476,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter partition"
expl=
"VC for partition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter partition.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"4"
/></proof>
</goal>
...
...
examples/algo64/why3session.xml
View file @
8e560e42
...
...
@@ -6,7 +6,7 @@
<file
name=
"../algo64.mlw"
>
<theory
name=
"Algo64"
>
<goal
name=
"WP_parameter quicksort"
expl=
"VC for quicksort"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter quicksort.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"5"
/></proof>
</goal>
...
...
@@ -43,7 +43,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter qs"
expl=
"VC for qs"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter qs.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"2"
/></proof>
</goal>
...
...
examples/algo65/why3session.xml
View file @
8e560e42
...
...
@@ -6,7 +6,7 @@
<file
name=
"../algo65.mlw"
>
<theory
name=
"Algo65"
>
<goal
name=
"WP_parameter find"
expl=
"VC for find"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter find.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.00"
steps=
"6"
/></proof>
</goal>
...
...
@@ -23,7 +23,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"96"
/></proof>
</goal>
<goal
name=
"WP_parameter find.6"
expl=
"assertion"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter find.6.1"
expl=
"assertion"
>
<proof
prover=
"1"
timelimit=
"6"
><result
status=
"valid"
time=
"0.22"
steps=
"248"
/></proof>
</goal>
...
...
@@ -90,7 +90,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
steps=
"163"
/></proof>
</goal>
<goal
name=
"WP_parameter find.26"
expl=
"assertion"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter find.26.1"
expl=
"assertion"
>
<proof
prover=
"1"
timelimit=
"6"
><result
status=
"valid"
time=
"0.30"
steps=
"380"
/></proof>
</goal>
...
...
examples/all_distinct/why3session.xml
View file @
8e560e42
...
...
@@ -6,7 +6,7 @@
<file
name=
"../all_distinct.mlw"
>
<theory
name=
"AllDistinct"
>
<goal
name=
"WP_parameter all_distinct"
expl=
"VC for all_distinct"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter all_distinct.1"
expl=
"array creation size"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"2"
/></proof>
</goal>
...
...
examples/arm/why3session.xml
View file @
8e560e42
...
...
@@ -7,7 +7,7 @@
<file
name=
"../arm.mlw"
>
<theory
name=
"M"
>
<goal
name=
"WP_parameter insertion_sort"
expl=
"VC for insertion_sort"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter insertion_sort.1"
expl=
"loop invariant init"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.00"
steps=
"6"
/></proof>
</goal>
...
...
examples/avl/association_list/why3session.xml
View file @
8e560e42
...
...
@@ -16,7 +16,7 @@
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
steps=
"103"
/></proof>
</goal>
<goal
name=
"WP_parameter model_congruence"
expl=
"VC for model_congruence"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter model_congruence.1"
expl=
"variant decrease"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.01"
steps=
"6"
/></proof>
</goal>
...
...
@@ -38,7 +38,7 @@
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
steps=
"70"
/></proof>
</goal>
<goal
name=
"WP_parameter model_concat"
expl=
"VC for model_concat"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter model_concat.1"
expl=
"postcondition"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
steps=
"24"
/></proof>
</goal>
...
...
@@ -89,12 +89,12 @@
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.07"
steps=
"66"
/></proof>
</goal>
<goal
name=
"WP_parameter model_cut"
expl=
"VC for model_cut"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter model_cut.1"
expl=
"assertion"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
steps=
"66"
/></proof>
</goal>
<goal
name=
"WP_parameter model_cut.2"
expl=
"assertion"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter model_cut.2.1"
expl=
"assertion"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
steps=
"25"
/></proof>
</goal>
...
...
@@ -116,7 +116,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter model_cut.3"
expl=
"assertion"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter model_cut.3.1"
expl=
"assertion"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
steps=
"25"
/></proof>
</goal>
...
...
@@ -138,7 +138,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter model_cut.4"
expl=
"assertion"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter model_cut.4.1"
expl=
"assertion"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
...
...
examples/avl/avl/why3session.xml
View file @
8e560e42
...
...
@@ -45,7 +45,7 @@
<proof
prover=
"1"
timelimit=
"2"
memlimit=
"0"
><result
status=
"valid"
time=
"0.07"
steps=
"257"
/></proof>
</goal>
<goal
name=
"WP_parameter balance"
expl=
"VC for balance"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter balance.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"5"
/></proof>
</goal>
...
...
@@ -196,7 +196,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"1"
/></proof>
</goal>
<goal
name=
"WP_parameter insert"
expl=
"VC for insert"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter insert.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
</goal>
...
...
@@ -272,7 +272,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter remove"
expl=
"VC for remove"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter remove.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
</goal>
...
...
@@ -351,7 +351,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.79"
steps=
"2065"
/></proof>
</goal>
<goal
name=
"WP_parameter extract"
expl=
"VC for extract"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter extract.1"
expl=
"precondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
</goal>
...
...
examples/avl/priority_queue/why3session.xml
View file @
8e560e42
...
...
@@ -12,7 +12,7 @@
<proof
prover=
"1"
timelimit=
"3"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
</goal>
<goal
name=
"WP_parameter assoc_m"
expl=
"VC for assoc_m"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter assoc_m.0"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
...
...
@@ -64,12 +64,12 @@
<proof
prover=
"1"
timelimit=
"3"
><result
status=
"valid"
time=
"0.03"
steps=
"3"
/></proof>
</goal>
<goal
name=
"WP_parameter monoid_sum_is_min"
expl=
"VC for monoid_sum_is_min"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter monoid_sum_is_min.0"
expl=
"variant decrease"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"6"
/></proof>
</goal>
<goal
name=
"WP_parameter monoid_sum_is_min.1"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter monoid_sum_is_min.1.0"
expl=
"VC for monoid_sum_is_min"
proved=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.13"
/></proof>
</goal>
...
...
@@ -87,7 +87,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter selected_is_min"
expl=
"VC for selected_is_min"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_is_min.0"
expl=
"unreachable point"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
</goal>
...
...
@@ -95,7 +95,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"13"
/></proof>
</goal>
<goal
name=
"WP_parameter selected_is_min.2"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_is_min.2.0"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"6"
/></proof>
</goal>
...
...
@@ -113,12 +113,12 @@
</transf>
</goal>
<goal
name=
"WP_parameter selected_part"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.0"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"47"
/></proof>
</goal>
<goal
name=
"WP_parameter selected_part.1"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.1.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
steps=
"114"
/></proof>
</goal>
...
...
@@ -134,7 +134,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"1.84"
steps=
"1561"
/></proof>
</goal>
<goal
name=
"WP_parameter selected_part.3"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.3.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"23"
/></proof>
</goal>
...
...
@@ -143,7 +143,7 @@
<goal
name=
"WP_parameter selected_part.3.1.0"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.3.1.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.3.1.0.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"13"
/></proof>
</goal>
...
...
@@ -165,7 +165,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter selected_part.4"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.4.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"23"
/></proof>
</goal>
...
...
@@ -174,7 +174,7 @@
<goal
name=
"WP_parameter selected_part.4.1.0"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.4.1.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.4.1.0.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"14"
/></proof>
</goal>
...
...
@@ -198,7 +198,7 @@
<goal
name=
"WP_parameter selected_part.4.3.0"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.4.3.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.4.3.0.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"15"
/></proof>
</goal>
...
...
@@ -219,7 +219,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter first_minimum_caracterisation"
expl=
"VC for first_minimum_caracterisation"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter first_minimum_caracterisation.0"
expl=
"unreachable point"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"3"
/></proof>
</goal>
...
...
@@ -254,7 +254,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.18"
steps=
"360"
/></proof>
</goal>
<goal
name=
"WP_parameter first_minimum_caracterisation.11"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter first_minimum_caracterisation.11.0"
expl=
"VC for first_minimum_caracterisation"
proved=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"1.05"
/></proof>
</goal>
...
...
@@ -267,7 +267,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
steps=
"93"
/></proof>
</goal>
<goal
name=
"WP_parameter first_minimum_caracterisation.13"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter first_minimum_caracterisation.13.0"
expl=
"VC for first_minimum_caracterisation"
proved=
"true"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.23"
/></proof>
</goal>
...
...
examples/avl/ral/why3session.xml
View file @
8e560e42
...
...
@@ -96,7 +96,7 @@
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"6"
/></proof>
</goal>
<goal
name=
"WP_parameter set"
expl=
"VC for set"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter set.1"
expl=
"precondition"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"8"
/></proof>
</goal>
...
...
@@ -127,7 +127,7 @@
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.05"
steps=
"59"
/></proof>
</goal>
<goal
name=
"WP_parameter harness"
expl=
"VC for harness"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter harness.1"
expl=
"precondition"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"5"
/></proof>
</goal>
...
...
@@ -161,7 +161,7 @@
</transf>
</goal>
<goal
name=
"WP_parameter harness2"
expl=
"VC for harness2"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter harness2.1"
expl=
"precondition"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.02"
steps=
"3"
/></proof>
</goal>
...
...
examples/avl/sorted/why3session.xml
View file @
8e560e42
...
...
@@ -12,7 +12,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"8"
/></proof>
</goal>
<goal
name=
"WP_parameter increasing_precede"
expl=
"VC for increasing_precede"
>
<transf
name=
"split_goal_
wp
"
>
<transf
name=
"split_goal_
right
"
>
<goal
name=
"WP_parameter increasing_precede.1"
expl=
"postcondition"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"14"
/></proof>
</goal>
...
...
examples/avl/tables/why3session.xml
View file @
8e560e42
...
...
@@ -44,7 +44,7 @@
<proof
prover=
"1"
timelimit=
"3"
><result
status=
"valid"
time=
"0.03"
steps=
"2"
/></proof>
</goal>
<goal
name=
"WP_parameter selected_sem"
expl=
"VC for selected_sem"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_sem.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"5"
/></proof>
</goal>
...
...
@@ -78,13 +78,13 @@
</transf>
</goal>
<goal
name=
"WP_parameter selected_part"
expl=
"VC for selected_part"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.0"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"introduce_premises"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.0.0"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.0.0.0"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.0.0.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.01"
steps=
"15"
/></proof>
</goal>
...
...
@@ -117,7 +117,7 @@
<goal
name=
"WP_parameter selected_part.1.0"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.1.0.0"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter selected_part.1.0.0.0"
expl=
"VC for selected_part"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"16"
/></proof>
</goal>
...
...
@@ -223,7 +223,7 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.17"
steps=
"417"
/></proof>
</goal>
<goal
name=
"WP_parameter add_max"
expl=
"VC for add_max"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter add_max.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"4"
/></proof>
</goal>
...
...
@@ -242,12 +242,12 @@
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.25"
steps=
"792"
/></proof>
</goal>
<goal
name=
"WP_parameter insert"
expl=
"VC for insert"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter insert.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.02"
steps=
"6"
/></proof>
</goal>
<goal
name=
"WP_parameter insert.1"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"split_goal_
wp
"
proved=
"true"
>
<transf
name=
"split_goal_
right
"
proved=
"true"
>
<goal
name=
"WP_parameter insert.1.0"
expl=
"VC for insert"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.36"
steps=
"411"
/></proof>