ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples
History
Johannes Kanig 25b13e2cab merge commit
2025-12-15 10:45:08 +09:00
..
add_list
add E prover 2.6
2025-12-11 10:29:15 +01:00
add_list_vc_sp
add E prover 2.6
2025-12-11 10:29:15 +01:00
algo63
update a session
2025-12-09 10:43:49 +01:00
algo64
upgraded provers in examples
2025-12-09 10:43:46 +01:00
algo65
upgraded provers in examples
2025-12-09 10:43:46 +01:00
all_distinct
upgraded provers in examples
2025-12-09 10:43:46 +01:00
alpha_beta
upgraded provers in examples
2025-12-09 10:43:46 +01:00
amortization
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
anagrammi
upgraded provers in examples
2025-12-09 10:43:46 +01:00
arm
upgraded provers in examples
2025-12-09 10:43:46 +01:00
array_most_frequent
upgraded provers in examples
2025-12-09 10:43:46 +01:00
array_of_list
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
assigning_meanings_to_programs
upgraded provers in examples
2025-12-09 10:43:46 +01:00
avl
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bag
upgraded provers in examples
2025-12-09 10:43:46 +01:00
balance
upgraded provers in examples
2025-12-09 10:43:46 +01:00
bellman_ford
fix mistake
2025-12-09 10:43:49 +01:00
bignum
upgraded provers in examples
2025-12-09 10:43:46 +01:00
binary_multiplication
upgraded provers in examples
2025-12-09 10:43:46 +01:00
binary_search
upgraded provers in examples
2025-12-09 10:43:46 +01:00
binary_search_vc_sp
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
binary_sort
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
binary_sqrt
upgraded provers in examples
2025-12-09 10:43:46 +01:00
binomial
fix cmd line for E-prover 3.x
2025-12-11 16:29:16 +01:00
binomial_heap
upgraded provers in examples
2025-12-09 10:43:46 +01:00
bitcount
upgraded provers in examples
2025-12-09 10:43:46 +01:00
bitvector_examples
upgraded provers in examples
2025-12-09 10:43:46 +01:00
bitvectors
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
bitwalker
upgraded provers in examples
2025-12-09 10:43:46 +01:00
braun_trees
upgraded provers in examples
2025-12-09 10:43:46 +01:00
bresenham
upgraded provers in examples
2025-12-09 10:43:46 +01:00
bts
reproducer and fix
2025-09-29 18:16:21 +02:00
bubble_sort
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
c_cursor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
check-builtin
unused dependencies on Euclidean div/mod
2024-10-23 15:10:58 +02:00
checking_a_large_routine
upgraded provers in examples
2025-12-09 10:43:46 +01:00
coincidence_count
upgraded provers in examples
2025-12-09 10:43:46 +01:00
coincidence_count_list
upgraded provers in examples
2025-12-09 10:43:46 +01:00
coma
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
conjugate
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
counting_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
cubic_root
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
cursor_examples
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
decrease1
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
defunctionalization
upgraded provers in examples
2025-12-09 10:43:46 +01:00
dfa_example
Remove unused proofs.
2024-12-07 09:01:55 +01:00
dfs
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
dijkstra
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
disamb
upgraded provers in examples
2025-12-09 10:43:46 +01:00
division
upgraded provers in examples
2025-12-09 10:43:46 +01:00
doc_examples
avoid iso-8859 encoding in examples
2025-11-27 09:49:14 +01:00
double_wp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
dyck
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
edit_distance
eprover and spass and Z3 4.14
2025-12-11 12:03:25 +01:00
equality_up_to_spaces
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
esterel
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler001
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler002
eprover and spass and Z3 4.14
2025-12-11 12:03:25 +01:00
euler011
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
euler_sieve
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
ewd673
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
f_puzzle
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fact
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fact_vc_sp
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
fenwick
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fib_memo
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fibonacci
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
fill
upgraded provers in examples
2025-12-09 10:43:46 +01:00
find
upgraded provers in examples
2025-12-09 10:43:46 +01:00
finger_trees
upgraded provers in examples
2025-12-09 10:43:46 +01:00
finite_tarski
upgraded provers in examples
2025-12-09 10:43:46 +01:00
flag
upgraded provers in examples
2025-12-09 10:43:46 +01:00
flag2
upgraded provers in examples
2025-12-09 10:43:46 +01:00
flexible_arrays
upgraded provers in examples
2025-12-09 10:43:46 +01:00
foveoos11_challenge1
upgraded provers in examples
2025-12-09 10:43:46 +01:00
foveoos11_challenge2
upgraded provers in examples
2025-12-09 10:43:46 +01:00
foveoos11_challenge3
upgraded provers in examples
2025-12-09 10:43:46 +01:00
foveoos11-cm
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
gcd
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
gcd_bezout
upgraded provers in examples
2025-12-09 10:43:46 +01:00
gcd_bezout_vc_sp
upgraded provers in examples
2025-12-09 10:43:46 +01:00
gcd_vc_sp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
generate_all_trees
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
gnome_sort
gnome-sort: improved variant
2025-10-15 09:48:01 +02:00
hackers-delight
upgraded provers in examples
2025-12-09 10:43:46 +01:00
hashtbl_impl
upgraded provers in examples
2025-12-09 10:43:46 +01:00
hillel_challenge
upgraded provers in examples
2025-12-09 10:43:46 +01:00
huffman_with_two_queues
a better theory seq.Sum
2025-12-03 19:01:11 +01:00
i_cant_believe_it_can_sort
upgraded provers in examples
2025-12-09 10:43:46 +01:00
induction
upgraded provers in examples
2025-12-09 10:43:46 +01:00
infinity_of_primes
upgraded provers in examples
2025-12-09 10:43:46 +01:00
insertion_sort
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
insertion_sort_list
fix cmd line for E-prover 3.x
2025-12-11 16:29:16 +01:00
insertion_sort_naive
upgraded provers in examples
2025-12-09 10:43:46 +01:00
inverse_in_place
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
isqrt
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
isqrt_von_neumann
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
just_join
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
kleene_algebra
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
kmp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
knuth_prime_numbers
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
koda_ruskey
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
largest_prime_factor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
lcp
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
leftist_heap
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
linear_probing
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
linked_list_rev
eprover and spass and Z3 4.14
2025-12-11 12:03:25 +01:00
list_removal
upgraded provers in examples
2025-12-09 10:43:46 +01:00
locate_max
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
logic
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
longest_increasing_subsequence
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
max_matrix
upgraded provers in examples
2025-12-09 10:43:46 +01:00
maximum_subarray
upgraded provers in examples
2025-12-09 10:43:46 +01:00
mccarthy
upgraded provers in examples
2025-12-09 10:43:46 +01:00
mccarthy_vc_sp
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
mergesort_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mergesort_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mergesort_queue
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
mex
more upgraded sessions
2025-12-09 10:43:49 +01:00
micro-c
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
min_max
more upgraded sessions
2025-12-09 10:43:49 +01:00
mjrty
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
mlcfg
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
muller
more upgraded sessions
2025-12-09 10:43:49 +01:00
multiprecision
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
mutual_recursion
more upgraded sessions
2025-12-09 10:43:49 +01:00
my_cosine
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
nistonacci
more upgraded sessions
2025-12-09 10:43:49 +01:00
numeric
relax hypothesis on a_max
2025-12-08 16:19:47 +01:00
optimal_replay
more upgraded sessions
2025-12-09 10:43:49 +01:00
pairing_heap
bench reduced using bench image with more provers
2025-12-11 18:25:13 +01:00
pairing_heap_bin
more upgraded sessions
2025-12-09 10:43:49 +01:00
pancake_sorting
more upgraded sessions
2025-12-09 10:43:49 +01:00
patience
more upgraded sessions
2025-12-09 10:43:49 +01:00
pigeonhole
more upgraded sessions
2025-12-09 10:43:49 +01:00
power
more upgraded sessions
2025-12-09 10:43:49 +01:00
power_vc_sp
more upgraded sessions
2025-12-09 10:43:49 +01:00
pqueue
eprover and spass and Z3 4.14
2025-12-11 12:03:25 +01:00
proper_cuts
more upgraded sessions
2025-12-09 10:43:49 +01:00
prover
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
python
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
queens
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
queens_bv
more upgraded sessions
2025-12-09 10:43:49 +01:00
queue_two_lists
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
quicksort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
random_access_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
register_allocation
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
relabel
list.Distinct using a recursive definition
2025-05-14 17:32:28 +02:00
remove_duplicate
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
remove_duplicate_hash
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
residual
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
resizable_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
rightmostbittrick
remove use of cvc5 1.2.0
2024-11-04 13:49:14 +01:00
ring_buffer
Fix type invariant for the ring buffer example
2025-11-07 14:29:31 +00:00
ring_decision
Do not introduce program variables for zero and one in int.Int module
2025-03-26 15:17:05 +01:00
ropes
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
same_fringe
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
schorr_waite
gallery: cleaning Schorr-Waite with autodereference and more recent provers
2025-11-18 09:44:26 +01:00
schorr_waite_via_recursion
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
schorr_waite_with_ghost_monitor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
search
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
selection_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
set_iterators
add simple examples of iterators on sets with extraction to OCaml
2025-03-26 17:20:01 +01:00
sf
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
sieve
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
skew_heaps
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
slowsort
new example: slowsort
2025-05-06 18:20:12 +02:00
snapshotable_trees
proper renaming of E prover 2.6
2025-12-11 13:58:58 +01:00
sorted_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
space_saving
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
split_string
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
sqrt2_irrational
sqrt 2 irrational simplified
2025-07-17 10:45:45 +02:00
stackify
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
stdlib
proved udivexact generique
2025-11-25 11:26:25 +01:00
stooge_sort
stooge_sort: simplified proof
2025-05-08 08:27:19 +02:00
string_base64_encoding
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
string_hex_encoding
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
string_search
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
subsequence
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
sudoku
Merge 1.8.2 into AdaCore master
2025-10-14 10:32:03 +09:00
sudoku2
yet another Sudoku solver
2025-10-08 11:16:11 +02:00
sumrange
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
swap
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tests
fix bench rac oracle
2025-03-26 19:31:07 +01:00
tests-provers
Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel
2025-03-25 17:48:51 +01:00
there_and_back_again
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
three_idem_ring
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
topological_sorting
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tortoise_and_hare
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tower_of_hanoi
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
toy_compiler
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
tree_height
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tree_of_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
tree_of_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
union_find
gallery: improved union-find
2025-09-02 15:19:50 +02:00
unraveling_a_card_trick
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
use_api
Fix API examples
2025-11-24 13:16:22 +01:00
vacid_0_binary_heaps
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vacid_0_build_maze
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vacid_0_red_black_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vacid_0_sparse_array
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2015_dancing_links
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2015_parallel_gcd
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
verifythis_2015_relaxed_prefix
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2016_matrix_multiplication
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2016_tree_traversal
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_maximum_sum_submatrix
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_odd_even_sort_rearranging
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_odd_even_transposition_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_pair_insertion_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2017_tree_buffer
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_array_based_queuing_lock_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_array_based_queuing_lock_2
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
verifythis_2018_le_rouge_et_le_noir_1
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
verifythis_2018_le_rouge_et_le_noir_2
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_mind_the_gap_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2018_mind_the_gap_2
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
verifythis_2018_register_allocation
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2019_cartesian_trees
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2019_ghc_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_dll_to_bst
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_lexicographic_permutations_1
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2021_lexicographic_permutations_2
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
verifythis_2021_shearsort
eprover and spass and Z3 4.14
2025-12-11 12:03:25 +01:00
verifythis_2021_shearsort_modified
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
verifythis_2024_challenge0
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_2024_challenge1
add metas for unused-dependencies on sequences
2024-10-29 16:12:46 +01:00
verifythis_fm2012_LRS
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
verifythis_fm2012_treedel
list.Distinct using a recursive definition
2025-05-14 17:32:28 +02:00
verifythis_PrefixSumRec
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_aqueue
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_inverting
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_max_sum
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
vstte10_queens
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte10_search_list
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte12_bfs
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte12_combinators
merge commit
2025-12-15 10:45:08 +09:00
vstte12_ring_buffer
fix sessions and CE oracles
2024-11-14 14:48:30 +01:00
vstte12_tree_reconstruction
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
vstte12_two_way_sort
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
warshall_algorithm
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
white_and_black_balls
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
word_common_factor
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
WP_revisited
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
wrap_lines
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
zeros
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
add_list_vc_sp.mlw
…
add_list.mlw
…
algo63.mlw
…
algo64.mlw
…
algo65.mlw
…
all_distinct.mlw
…
alpha_beta.mlw
new example: alpha-beta
2025-03-21 10:08:09 +01:00
amortization.mlw
a simple example of amortization
2021-04-01 13:47:23 +02:00
anagrammi.mlw
anagrammi: fixed BASIC code
2024-04-05 18:05:12 +02:00
arm.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
array_most_frequent.mlw
examples: updated files for the gallery
2020-03-04 15:56:23 +01:00
array_of_list.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
assigning_meanings_to_programs.mlw
gallery: more auto-dereference
2024-01-23 19:09:26 +01:00
bag.mlw
fix proofs, including one failing with Coq 8.19
2024-06-21 15:54:38 +02:00
balance.mlw
gallery: improve balance example even more
2023-04-07 10:59:08 +02:00
bellman_ford.mlw
no more libraries appmap and impmap
2020-02-11 17:56:34 +01:00
bench.sh
…
bignum.mlw
…
binary_multiplication.mlw
…
binary_search_vc_sp.mlw
…
binary_search.mlw
new example: search in a two-dimensional grid
2024-07-06 12:13:17 +02:00
binary_sort.mlw
…
binary_sqrt.mlw
…
binomial_heap.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
binomial.mlw
binomial coefficient example: alternative loop
2025-05-20 14:35:38 +02:00
bitcount.mlw
Several renamings and fix a few pre and post-conditions
2021-09-29 08:57:02 +02:00
bitvector_examples.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
bitwalker.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
braun_trees.mlw
gallery: two return types added
2022-12-01 20:02:29 +01:00
bresenham.mlw
…
bubble_sort.mlw
new example: Knuth's bubble sort
2024-09-05 19:11:32 +02:00
checking_a_large_routine.mlw
examples: variant of Turing's factorial
2022-08-26 11:27:04 +02:00
coincidence_count_list.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
coincidence_count.mlw
ease the proof of coincidence count
2024-11-15 15:39:22 +01:00
conjugate.mlw
conjugate: a 32-bit implementation, which extracts to C
2019-07-04 16:39:58 +02:00
counting_sort.mlw
…
cubic_root.mlw
example cubic_root: nicer code using auto deref
2020-03-04 16:11:49 +01:00
cursor_examples.mlw
Use interfaces in cursor_examples.mlw
2023-05-23 13:27:45 +02:00
decrease1.mlw
…
defunctionalization.mlw
…
dfa_example.mlw
stdlib: update Regexp to use sequences
2024-03-20 18:13:00 +01:00
dfs.mlw
…
dijkstra.mlw
no more libraries appmap and impmap
2020-02-11 17:56:34 +01:00
disamb.mlw
more comments on the disamb example
2020-10-01 15:50:36 +02:00
division.mlw
Do not introduce program variables for zero and one in int.Int module
2025-03-26 15:17:05 +01:00
dyck.mlw
…
edit_distance.mlw
…
equality_up_to_spaces.mlw
Fix examples so they don't define type string
2019-09-23 11:14:46 +02:00
esterel.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
euler001.mlw
Remove some trailing spaces.
2024-12-07 09:01:55 +01:00
euler002.mlw
…
euler011.mlw
…
euler_sieve.mlw
fix sessions
2021-06-25 14:15:38 +02:00
ewd673.mlw
…
f_puzzle.mlw
Change extension to mlw.
2020-03-05 09:17:48 +01:00
fact_vc_sp.mlw
…
fact.mlw
…
fenwick.mlw
…
fib_memo.mlw
…
fibonacci.mlw
gallery: a small result about Fibonacci numbers
2024-10-16 10:48:25 +02:00
fill.mlw
…
find.mlw
…
finger_trees.mlw
…
finite_tarski.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
flag2.mlw
…
flag.mlw
…
flexible_arrays.mlw
flexible arrays: more operations
2023-04-18 14:35:23 +02:00
foveoos11_challenge1.mlw
…
foveoos11_challenge2.mlw
upgraded provers in examples
2025-12-09 10:43:46 +01:00
foveoos11_challenge3.mlw
…
gcd_bezout_vc_sp.mlw
…
gcd_bezout.mlw
…
gcd_vc_sp.mlw
…
gcd.mlw
more autodereference in the gallery
2020-06-25 10:49:12 +02:00
generate_all_trees.mlw
…
gnome_sort.mlw
gnome-sort: improved variant
2025-10-15 09:48:01 +02:00
hackers-delight.mlw
…
hashtbl_impl.mlw
…
hello-world.mlw
Printer for string literals with escape sequences.
2019-10-22 16:26:19 +02:00
hillel_challenge.mlw
stdlib: new library fmap
2019-11-08 16:59:54 +01:00
huffman_with_two_queues.mlw
a better theory seq.Sum
2025-12-03 19:01:11 +01:00
i_cant_believe_it_can_sort.mlw
cleaning up
2022-07-04 11:28:47 +02:00
incremental.mlw
…
induction.mlw
…
infinity_of_primes.mlw
new example: infinity_of_primes
2021-06-11 14:37:03 +02:00
insertion_sort_list.mlw
vc: extend default wf-ordering for algebraic variants
2025-07-08 16:25:03 +02:00
insertion_sort_naive.mlw
insertion_sort: cleaning up, auto deref, swap version
2021-03-18 18:33:45 +01:00
insertion_sort.mlw
insertion_sort: cleaning up, auto deref, swap version
2021-03-18 18:33:45 +01:00
inverse_in_place.mlw
inverse_in_place with auto-dereference
2019-07-04 10:39:55 +02:00
isqrt_von_neumann.mlw
example isqrt von neumann: improve comments
2020-03-04 16:21:29 +01:00
isqrt.mlw
add default names for program annotations
2019-06-07 15:06:30 +02:00
just_join.mlw
Do not remove properties of bv.Pow2 systematically
2024-10-04 16:35:37 +02:00
kleene_algebra.mlw
fix realizations
2024-11-13 19:10:42 +01:00
kmp.mlw
…
knuth_prime_numbers.mlw
…
koda_ruskey.mlw
…
largest_prime_factor.mlw
…
lcp.mlw
…
leftist_heap.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
linear_probing.mlw
…
linked_list_rev.mlw
gallery: list reversal terminates, even on cyclic lists
2022-11-06 00:02:54 +01:00
list_removal.mlw
one writes in enough
2021-03-16 14:55:20 +01:00
locate_max.mlw
Document the extraction to C.
2022-05-11 17:46:27 +02:00
longest_increasing_subsequence.mlw
new example: longest increasing subsequence
2024-05-05 16:05:20 +02:00
max_matrix.mlw
no more theory sum.Sum
2020-02-12 10:30:25 +01:00
maximum_subarray.mlw
examples: variant of Kadane's algorithm
2024-02-11 19:11:47 +01:00
mccarthy_vc_sp.mlw
…
mccarthy.mlw
…
mergesort_array.mlw
…
mergesort_list.mlw
…
mergesort_queue.mlw
updated proof sessions
2019-06-05 17:55:47 +02:00
mex.mlw
minimum excludant example
2025-02-01 21:22:20 +01:00
min_max.mlw
min_max: a divide and conquer solution
2020-02-14 09:06:31 +01:00
mjrty.mlw
new example: space saving algorithm
2023-05-09 15:54:05 +02:00
muller.mlw
…
mutual_recursion.mlw
modified example mutual_recursion
2020-05-01 21:05:40 +02:00
my_cosine.mlw
…
nistonacci.mlw
…
optimal_replay.mlw
…
pairing_heap_bin.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
pairing_heap.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
pancake_sorting.mlw
…
patience.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
pigeonhole.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
power_vc_sp.mlw
…
power.mlw
example power: cleaning up, new version
2023-07-25 10:48:55 +02:00
pqueue.mlw
rendons à César...
2025-11-21 13:26:28 +01:00
proper_cuts.mlw
new example: proper cuts
2024-05-02 10:22:45 +02:00
queens_bv.mlw
Resolve "Give values to BV constants when cloning"
2023-06-16 08:44:32 +00:00
queens.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
queue_two_lists.mlw
Merge remote-tracking branch 'origin/master' into fixclone
2020-03-16 20:52:59 +01:00
quicksort.mlw
examples: yet another version of quicksort
2021-01-13 11:10:32 +01:00
random_access_list.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
reduced_regtests.list
Remove rightmostbittrick from CI, as it fails a bit too often.
2019-11-15 14:45:54 +01:00
register_allocation.mlw
…
regtests.out
Fix sessions and update oracles for result variables in VC SP
2021-10-04 15:53:08 +02:00
regtests.sh
more provers, replay restricted to real examples
2025-12-09 10:42:26 +01:00
relabel.mlw
…
remove_duplicate_hash.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
remove_duplicate.mlw
…
residual.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
resizable_array.mlw
Dexpr: emit a warning for spurious olds in val contracts
2021-03-12 20:56:41 +01:00
rightmostbittrick.mlw
improved proof
2024-11-03 19:28:33 +01:00
ring_buffer.mlw
Fix type invariant for the ring buffer example
2025-11-07 14:29:31 +00:00
ropes.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
same_fringe.mlw
…
schorr_waite_via_recursion.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
schorr_waite_with_ghost_monitor.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
schorr_waite.mlw
gallery: cleaning Schorr-Waite with autodereference and more recent provers
2025-11-18 09:44:26 +01:00
search.mlw
cleaning up
2023-12-14 20:01:43 +01:00
selection_sort.mlw
…
set_iterators.mlw
add simple examples of iterators on sets with extraction to OCaml
2025-03-26 17:20:01 +01:00
sf.mlw
…
sieve.mlw
…
skew_heaps.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
slowsort.mlw
new example: slowsort
2025-05-06 18:20:12 +02:00
snapshotable_trees.mlw
…
sorted_list.mlw
…
space_saving.mlw
Fix typos.
2023-11-23 18:38:17 +01:00
split_string.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
sqrt2_irrational.mlw
sqrt 2 irrational simplified
2025-07-17 10:45:45 +02:00
stooge_sort.mlw
stooge_sort: simplified proof
2025-05-08 08:27:19 +02:00
string_base64_encoding.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
string_hex_encoding.mlw
do not allow implicit inference of partial
2024-10-31 15:27:09 +01:00
string_search.mlw
update sessions
2024-11-03 11:48:13 +01:00
subsequence.mlw
new example: longest increasing subsequence
2024-05-05 16:05:20 +02:00
sudoku2.mlw
yet another Sudoku solver
2025-10-08 11:16:11 +02:00
sudoku.mlw
Fix occurrences of "occurences".
2023-11-23 19:04:11 +01:00
sumrange.mlw
…
swap.mlw
example: swapping two integers
2020-04-29 13:12:53 +02:00
there_and_back_again.mlw
…
three_idem_ring.mlw
Unified format for new examples
2019-11-06 15:47:00 +01:00
TODO
…
topological_sorting.mlw
no more libraries appmap and impmap
2020-02-11 17:56:34 +01:00
tortoise_and_hare.mlw
fix sessions
2021-06-25 15:01:56 +02:00
tower_of_hanoi.mlw
…
toy_compiler.mlw
toy compiler example: cleaning and documentation
2024-04-10 12:52:40 +02:00
tree_height.mlw
…
tree_of_array.mlw
…
tree_of_list.mlw
…
union_find.mlw
avoid iso-8859 encoding in examples
2025-11-27 09:49:14 +01:00
unraveling_a_card_trick.mlw
…
vacid_0_build_maze.mlw
…
vacid_0_red_black_trees.mlw
…
vacid_0_sparse_array.mlw
…
verifythis_2015_dancing_links.mlw
…
verifythis_2015_parallel_gcd.mlw
…
verifythis_2015_relaxed_prefix.mlw
…
verifythis_2016_tree_traversal.mlw
…
verifythis_2017_maximum_sum_submatrix.mlw
…
verifythis_2017_odd_even_sort_rearranging.mlw
…
verifythis_2017_odd_even_transposition_sort.mlw
…
verifythis_2017_pair_insertion_sort.mlw
…
verifythis_2017_tree_buffer.mlw
…
verifythis_2018_array_based_queuing_lock_1.mlw
…
verifythis_2018_array_based_queuing_lock_2.mlw
Update ABQL session
2019-06-06 16:39:35 +02:00
verifythis_2018_le_rouge_et_le_noir_1.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
verifythis_2018_le_rouge_et_le_noir_2.mlw
examples/ fix name-shadowing conflicts due to the new Array.empty
2019-06-24 18:12:57 +02:00
verifythis_2018_mind_the_gap_1.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
verifythis_2018_mind_the_gap_2.mlw
…
verifythis_2018_register_allocation.mlw
simplifies fib tail rec proof and add counterexample to regalloc as a comment
2021-09-16 16:33:30 +02:00
verifythis_2019_cartesian_trees.mlw
Unified format for new examples
2019-11-06 15:47:00 +01:00
verifythis_2019_ghc_sort.mlw
Unified format for new examples
2019-11-06 15:47:00 +01:00
verifythis_2021_dll_to_bst.mlw
typo
2023-02-17 13:32:33 +01:00
verifythis_2021_lexicographic_permutations_1.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2021_lexicographic_permutations_2.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2021_shearsort_modified.mlw
fix euler_sieve, array and split_vc interaction
2021-04-30 10:48:03 +02:00
verifythis_2021_shearsort.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2024_challenge0.mlw
Do not remove properties of bv.Pow2 systematically
2024-10-04 16:35:37 +02:00
verifythis_2024_challenge1.mlw
Remove some trailing spaces.
2024-12-07 09:01:55 +01:00
verifythis_fm2012_LRS.mlw
Remove some trailing whitespaces.
2023-11-23 18:46:29 +01:00
verifythis_fm2012_treedel.mlw
…
verifythis_PrefixSumRec.mlw
…
vstte10_aqueue.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
vstte10_inverting.mlw
…
vstte10_max_sum.mlw
do not map IEEE floats theory to Alt-Ergo's own theory
2025-06-18 10:45:29 +09:00
vstte10_queens.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
vstte10_search_list.mlw
…
vstte12_bfs.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
vstte12_combinators.mlw
support for algebraic types simplify some proofs.
2023-01-31 08:25:07 +01:00
vstte12_ring_buffer.mlw
…
vstte12_tree_reconstruction.mlw
vstte12_tree_reconstruction: fix Coq proof
2019-08-21 12:55:22 +02:00
vstte12_two_way_sort.mlw
…
warshall_algorithm.mlw
…
white_and_black_balls.mlw
example white_and_black_balls: nicer code using auto deref
2020-03-04 16:48:11 +01:00
word_common_factor.mlw
word_common_factor: simplified proof
2019-04-02 17:30:14 +02:00
wrap_lines.mlw
examples/wrap_lines: extended challenge
2021-03-27 19:48:42 +01:00
zeros.mlw
…