This directory contains the specification and implementation files
for the following algorithms: Find, Find_First_Of,
Adjacent_Find, Equal, Search, Search_N, Find_End and
Count. These algorithms deal with arrays, but do not modify their
parameters.
As usual, ghost functions used in specifications are located in the
spec directory at project root.
The functions and the corresponding files are presented in the following table (click on the links to have more details on the specification/implementation of each function):
| function | files | comments |
|---|---|---|
| Find | naive_find_p.ads | a first naive version of Find |
naive_find_p.adb | ||
naive_find_contract_pb.ads | a simple example of contract with completeness/disjointedness problems | |
../spec/has_value_p.ads | the specification of the Has_Value predicate | |
find_p.ads | the final version of Find | |
find_p.adb | ||
| Find_First_Of | ../spec/has_value_of_p.ads | |
find_first_of_p.ads | ||
find_first_of_p.adb | ||
| Adjacent_Find | ../spec/has_equal_neighbors_p.ads | |
adjacent_find_p.ads | ||
adjacent_find_p.adb | ||
| Equal and Mismatch | ../spec/equal_ranges_p.ads | |
mismatch_p.ads | ||
mismatch_p.adb | ||
equal_p.ads | ||
equal_p.adb | ||
equal_rev_p.ads | another specification and implementation of Equal | |
| Search | search_wo_ghost.ads | a first specification and implementation without ghost functions |
search_wo_ghost.adb | ||
search_with_ghost.ads | a try to “naively” use ghost functions | |
search_with_ghost.adb | ||
../spec/has_sub_range_p.ads | the correct specification and implementation (thanks to Yannick Moy) | |
search_p.ads | ||
search_p.adb | ||
| Search_N | ../spec/has_constant_subrange_p.ads | |
search_n_p.ads | ||
search_n_p.adb | ||
| Find_End | find_end_p.ads | |
find_end_p.adb | ||
../spec/has_subrange_p.ads | ||
| Count | count_p.ads | |
count_p.adb | ||
../spec/occ_p.ads |