Index of /data/main/w/why3/1.8.0-2/examples

• Parent Directory
• TODO
• WP_revisited/
• add_list.mlw
• add_list/
• add_list_vc_sp.mlw
• add_list_vc_sp/
• algo63.mlw
• algo63/
• algo64.mlw
• algo64/
• algo65.mlw
• algo65/
• all_distinct.mlw
• all_distinct/
• amortization.mlw
• amortization/
• anagrammi.mlw
• anagrammi/
• arm.mlw
• arm/
• array_most_frequent.mlw
• array_most_frequent/
• array_of_list.mlw
• array_of_list/
• assigning_meanings_to_programs.mlw
• assigning_meanings_to_programs/
• avl/
• bag.mlw
• bag/
• balance.mlw
• balance/
• bellman_ford.mlw
• bellman_ford/
• bench.sh
• bignum.mlw
• bignum/
• binary_multiplication.mlw
• binary_multiplication/
• binary_search.mlw
• binary_search/
• binary_search_vc_sp.mlw
• binary_search_vc_sp/
• binary_sort.mlw
• binary_sort/
• binary_sqrt.mlw
• binary_sqrt/
• binomial.mlw
• binomial/
• binomial_heap.mlw
• binomial_heap/
• bitcount.mlw
• bitcount/
• bitvector_examples.mlw
• bitvector_examples/
• bitvectors/
• bitwalker.mlw
• bitwalker/
• braun_trees.mlw
• braun_trees/
• bresenham.mlw
• bresenham/
• bts/
• bubble_sort.mlw
• bubble_sort/
• c_cursor/
• check-builtin/
• checking_a_large_routine.mlw
• checking_a_large_routine/
• coincidence_count.mlw
• coincidence_count/
• coincidence_count_list.mlw
• coincidence_count_list/
• coma/
• conjugate.mlw
• conjugate/
• counting_sort.mlw
• counting_sort/
• cubic_root.mlw
• cubic_root/
• cursor_examples.mlw
• cursor_examples/
• decrease1.mlw
• decrease1/
• defunctionalization.mlw
• defunctionalization/
• dfa_example.mlw
• dfa_example/
• dfs.mlw
• dfs/
• dijkstra.mlw
• dijkstra/
• disamb.mlw
• disamb/
• division.mlw
• division/
• doc_examples/
• double_wp/
• dyck.mlw
• dyck/
• edit_distance.mlw
• edit_distance/
• equality_up_to_spaces.mlw
• equality_up_to_spaces/
• esterel.mlw
• esterel/
• euler001.mlw
• euler001/
• euler002.mlw
• euler002/
• euler011.mlw
• euler011/
• euler_sieve.mlw
• euler_sieve/
• ewd673.mlw
• ewd673/
• f_puzzle.mlw
• f_puzzle/
• fact.mlw
• fact/
• fact_vc_sp.mlw
• fact_vc_sp/
• fenwick.mlw
• fenwick/
• fib_memo.mlw
• fib_memo/
• fibonacci.mlw
• fibonacci/
• fill.mlw
• fill/
• find.mlw
• find/
• finger_trees.mlw
• finger_trees/
• finite_tarski.mlw
• finite_tarski/
• flag.mlw
• flag/
• flag2.mlw
• flag2/
• flexible_arrays.mlw
• flexible_arrays/
• foveoos11-cm/
• foveoos11_challenge1.mlw
• foveoos11_challenge1/
• foveoos11_challenge2.mlw
• foveoos11_challenge2/
• foveoos11_challenge3.mlw
• foveoos11_challenge3/
• gcd.mlw
• gcd/
• gcd_bezout.mlw
• gcd_bezout/
• gcd_bezout_vc_sp.mlw
• gcd_bezout_vc_sp/
• gcd_vc_sp.mlw
• gcd_vc_sp/
• generate_all_trees.mlw
• generate_all_trees/
• gnome_sort.mlw
• gnome_sort/
• hackers-delight.mlw
• hackers-delight/
• hashtbl_impl.mlw
• hashtbl_impl/
• hello-world.mlw
• hillel_challenge.mlw
• hillel_challenge/
• huffman_with_two_queues.mlw
• huffman_with_two_queues/
• i_cant_believe_it_can_sort.mlw
• i_cant_believe_it_can_sort/
• incremental.mlw
• induction.mlw
• induction/
• infinity_of_primes.mlw
• infinity_of_primes/
• insertion_sort.mlw
• insertion_sort/
• insertion_sort_list.mlw
• insertion_sort_list/
• insertion_sort_naive.mlw
• insertion_sort_naive/
• inverse_in_place.mlw
• inverse_in_place/
• isqrt.mlw
• isqrt/
• isqrt_von_neumann.mlw
• isqrt_von_neumann/
• just_join.mlw
• just_join/
• kleene_algebra.mlw
• kleene_algebra/
• kmp.mlw
• kmp/
• knuth_prime_numbers.mlw
• knuth_prime_numbers/
• koda_ruskey.mlw
• koda_ruskey/
• largest_prime_factor.mlw
• largest_prime_factor/
• lcp.mlw
• lcp/
• leftist_heap.mlw
• leftist_heap/
• linear_probing.mlw
• linear_probing/
• linked_list_rev.mlw
• linked_list_rev/
• list_removal.mlw
• list_removal/
• locate_max.mlw
• locate_max/
• logic/
• longest_increasing_subsequence.mlw
• longest_increasing_subsequence/
• max_matrix.mlw
• max_matrix/
• maximum_subarray.mlw
• maximum_subarray/
• mccarthy.mlw
• mccarthy/
• mccarthy_vc_sp.mlw
• mccarthy_vc_sp/
• mergesort_array.mlw
• mergesort_array/
• mergesort_list.mlw
• mergesort_list/
• mergesort_queue.mlw
• mergesort_queue/
• mex.mlw
• mex/
• micro-c/
• min_max.mlw
• min_max/
• mjrty.mlw
• mjrty/
• mlcfg/
• muller.mlw
• muller/
• multiprecision/
• mutual_recursion.mlw
• mutual_recursion/
• my_cosine.mlw
• my_cosine/
• nistonacci.mlw
• nistonacci/
• numeric/
• optimal_replay.mlw
• optimal_replay/
• pairing_heap.mlw
• pairing_heap/
• pairing_heap_bin.mlw
• pairing_heap_bin/
• pancake_sorting.mlw
• pancake_sorting/
• patience.mlw
• patience/
• pigeonhole.mlw
• pigeonhole/
• power.mlw
• power/
• power_vc_sp.mlw
• power_vc_sp/
• proper_cuts.mlw
• proper_cuts/
• prover/
• python/
• queens.mlw
• queens/
• queens_bv.mlw
• queens_bv/
• queue_two_lists.mlw
• queue_two_lists/
• quicksort.mlw
• quicksort/
• random_access_list.mlw
• random_access_list/
• reduced_regtests.list
• register_allocation.mlw
• register_allocation/
• regtests.out
• regtests.sh
• relabel.mlw
• relabel/
• remove_duplicate.mlw
• remove_duplicate/
• remove_duplicate_hash.mlw
• remove_duplicate_hash/
• residual.mlw
• residual/
• resizable_array.mlw
• resizable_array/
• rightmostbittrick.mlw
• rightmostbittrick/
• ring_buffer.mlw
• ring_buffer/
• ring_decision/
• ropes.mlw
• ropes/
• same_fringe.mlw
• same_fringe/
• schorr_waite.mlw
• schorr_waite/
• schorr_waite_via_recursion.mlw
• schorr_waite_via_recursion/
• schorr_waite_with_ghost_monitor.mlw
• schorr_waite_with_ghost_monitor/
• search.mlw
• search/
• selection_sort.mlw
• selection_sort/
• sf.mlw
• sf/
• sieve.mlw
• sieve/
• skew_heaps.mlw
• skew_heaps/
• snapshotable_trees.mlw
• snapshotable_trees/
• sorted_list.mlw
• sorted_list/
• space_saving.mlw
• space_saving/
• split_string.mlw
• split_string/
• stackify/
• stdlib/
• string_base64_encoding.mlw
• string_base64_encoding/
• string_hex_encoding.mlw
• string_hex_encoding/
• string_search.mlw
• string_search/
• subsequence.mlw
• subsequence/
• sudoku.mlw
• sudoku/
• sumrange.mlw
• sumrange/
• swap.mlw
• swap/
• tests-provers/
• tests/
• there_and_back_again.mlw
• there_and_back_again/
• three_idem_ring.mlw
• three_idem_ring/
• topological_sorting.mlw
• topological_sorting/
• tortoise_and_hare.mlw
• tortoise_and_hare/
• tower_of_hanoi.mlw
• tower_of_hanoi/
• toy_compiler.mlw
• toy_compiler/
• tree_height.mlw
• tree_height/
• tree_of_array.mlw
• tree_of_array/
• tree_of_list.mlw
• tree_of_list/
• unraveling_a_card_trick.mlw
• unraveling_a_card_trick/
• use_api/
• vacid_0_binary_heaps/
• vacid_0_build_maze.mlw
• vacid_0_build_maze/
• vacid_0_red_black_trees.mlw
• vacid_0_red_black_trees/
• vacid_0_sparse_array.mlw
• vacid_0_sparse_array/
• verifythis_2015_dancing_links.mlw
• verifythis_2015_dancing_links/
• verifythis_2015_parallel_gcd.mlw
• verifythis_2015_parallel_gcd/
• verifythis_2015_relaxed_prefix.mlw
• verifythis_2015_relaxed_prefix/
• verifythis_2016_matrix_multiplication/
• verifythis_2016_tree_traversal.mlw
• verifythis_2016_tree_traversal/
• verifythis_2017_maximum_sum_submatrix.mlw
• verifythis_2017_maximum_sum_submatrix/
• verifythis_2017_odd_even_sort_rearranging.mlw
• verifythis_2017_odd_even_sort_rearranging/
• verifythis_2017_odd_even_transposition_sort.mlw
• verifythis_2017_odd_even_transposition_sort/
• verifythis_2017_pair_insertion_sort.mlw
• verifythis_2017_pair_insertion_sort/
• verifythis_2017_tree_buffer.mlw
• verifythis_2017_tree_buffer/
• verifythis_2018_array_based_queuing_lock_1.mlw
• verifythis_2018_array_based_queuing_lock_1/
• verifythis_2018_array_based_queuing_lock_2.mlw
• verifythis_2018_array_based_queuing_lock_2/
• verifythis_2018_le_rouge_et_le_noir_1.mlw
• verifythis_2018_le_rouge_et_le_noir_1/
• verifythis_2018_le_rouge_et_le_noir_2.mlw
• verifythis_2018_le_rouge_et_le_noir_2/
• verifythis_2018_mind_the_gap_1.mlw
• verifythis_2018_mind_the_gap_1/
• verifythis_2018_mind_the_gap_2.mlw
• verifythis_2018_mind_the_gap_2/
• verifythis_2018_register_allocation.mlw
• verifythis_2018_register_allocation/
• verifythis_2019_cartesian_trees.mlw
• verifythis_2019_cartesian_trees/
• verifythis_2019_ghc_sort.mlw
• verifythis_2019_ghc_sort/
• verifythis_2021_dll_to_bst.mlw
• verifythis_2021_dll_to_bst/
• verifythis_2021_lexicographic_permutations_1.mlw
• verifythis_2021_lexicographic_permutations_1/
• verifythis_2021_lexicographic_permutations_2.mlw
• verifythis_2021_lexicographic_permutations_2/
• verifythis_2021_shearsort.mlw
• verifythis_2021_shearsort/
• verifythis_2021_shearsort_modified.mlw
• verifythis_2021_shearsort_modified/
• verifythis_2024_challenge0.mlw
• verifythis_2024_challenge0/
• verifythis_2024_challenge1.mlw
• verifythis_2024_challenge1/
• verifythis_PrefixSumRec.mlw
• verifythis_PrefixSumRec/
• verifythis_fm2012_LRS.mlw
• verifythis_fm2012_LRS/
• verifythis_fm2012_treedel.mlw
• verifythis_fm2012_treedel/
• vstte10_aqueue.mlw
• vstte10_aqueue/
• vstte10_inverting.mlw
• vstte10_inverting/
• vstte10_max_sum.mlw
• vstte10_max_sum/
• vstte10_queens.mlw
• vstte10_queens/
• vstte10_search_list.mlw
• vstte10_search_list/
• vstte12_bfs.mlw
• vstte12_bfs/
• vstte12_combinators.mlw
• vstte12_combinators/
• vstte12_ring_buffer.mlw
• vstte12_ring_buffer/
• vstte12_tree_reconstruction.mlw
• vstte12_tree_reconstruction/
• vstte12_two_way_sort.mlw
• vstte12_two_way_sort/
• warshall_algorithm.mlw
• warshall_algorithm/
• white_and_black_balls.mlw
• white_and_black_balls/
• word_common_factor.mlw
• word_common_factor/
• wrap_lines.mlw
• wrap_lines/
• zeros.mlw
• zeros/