This directory contains the specification and implementation files
for the following algorithms: Fill, Swap, Swap_Ranges, Copy,
Reverse_Copy, Reverse_In_Place, Rotate_Copy, Rotate,
Replace_Copy, Replace, Remove_Copy, Random_Shuffle. These
algorithms are particular, as they modify at least one of their
parameters.
As usual, ghost functions used in specifications are located in the
spec directory at project root. Lemmas needed to prove properties
are located in the lemmas directory at project root.
The functions and the corresponding files are presented in the following table (click on the link to have more details one the specification/implementation of each function):
| function | files | comments |
|---|---|---|
| Fill | ../spec/has_constant_subrange_p.ads | |
fill_p.ads | ||
fill_p.adb | ||
| Swap | swap_p.ads | |
swap_p.adb | ||
| Swap_Ranges | swap_p.ads | |
swap_p.adb | ||
swap_ranges_p.ads | ||
swap_ranges_p.adb | ||
swap_ranges_index_p.ads | a more SPARKish implementation | |
swap_ranges_index_p.adb | ||
| Copy | ../binary-search/equal_ranges_p.ads | |
../binary-search/equal_ranges_p.adb | ||
copy_p.ads | ||
copy_p.adb | ||
| Reverse_Copy | ../spec/is_reversed_p.ads | |
reverse_copy_p.ads | ||
reverse_copy_p.adb | ||
| Reverse_In_Place | ../spec/is_reversed_p.ads | |
swap_p.ads | ||
swap_p.adb | ||
reverse_in_place_swap_p.ads | a first version using Swap | |
reverse_in_place_swap_p.adb | ||
reverse_in_place_p.ads | ||
reverse_in_place_p.adb | ||
| Rotate_Copy | copy_p.ads | |
copy_p.adb | ||
rotate_copy_p.ads | ||
rotate_copy_p.adb | ||
| Rotate | reverse_in_place_p.ads | |
reverse_in_place_p.adb | ||
rotate_p.ads | ||
rotate_p.adb | ||
| Replace_Copy | ../spec/is_replaced_p.ads | |
replace_copy_p.ads | ||
replace_copy_p.adb | ||
| Replace | ../spec/is_replaced_p.ads | |
replace_p.ads | ||
replace_p.adb | ||
| Remove_Copy | ../spec/multiset_predicates.ads | |
../spec/remove_count_p.ads | ||
../spec/occ_p.ads | ||
../lemmas/remove_copy_lemmas.ads | ||
../lemmas/remove_copy_lemmas.adb | ||
remove_copy_first_p.ads | a first attempt to prove remove_copy | |
remove_copy_first_p.adb | ||
remove_copy_second_p.ads | a second attempt to prove remove_copy using lemmas | |
remove_copy_second_p.adb | ||
remove_copy_p.ads | final implementation of remove_copy | |
remove_copy_p.adb | ||
| Random_Shuffle | ../spec/multiset_predicates.ads | |
../lemmas/classic_lemmas.ads | ||
../lemmas/classic_lemmas.adb | ||
swap_array_p.ads | ||
swap_array_p.adb | ||
random_shuffle_p.ads | ||
random_shuffle_p.adb | ||
random_p.ads | ||
random_p.adb |