This directory contains the specification and implementation files
for the following algorithms: Search_Lower_Bound,
Search_Upper_Bound, Search_Equal_Ranges and
Binary_Search. These algorithms take sorted arrays as
parameters. The classic binary search is presented in this chapter.
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 one the specification/implementation of each function):
| function | files | comments |
|---|---|---|
| Search_Lower_Bound | ../spec/sorted_p.ads | |
../spec/lower_bound_p.ads | ||
../spec/upper_bound_p.ads | ||
search_lower_bound_p.ads | ||
search_lower_bound_p.adb | ||
| Search_Upper_Bound | ../spec/sorted_p.ads | |
../spec/lower_bound_p.ads | ||
../spec/upper_bound_p.ads | ||
search_upper_bound_p.ads | ||
search_upper_bound_p.adb | ||
| Search_Equal_Range | ../spec/sorted_p.ads | This function has two differents implementations: |
../spec/lower_bound_p.ads | the first version reuses the two previous algorithms, | |
../spec/upper_bound_p.ads | the second one is more efficient. | |
../spec/constant_range_p.ads | ||
search_lower_bound_p.ads | ||
search_lower_bound_p.adb | ||
search_upper_bound_p.ads | ||
search_upper_bound_p.adb | ||
search_equal_range_p.ads | ||
search_equal_range_p.adb | ||
search_equal_range_opt_p.ads | ||
saerch_equal_range_opt_p.adb | ||
| Binary_Search | ../spec/sorted_p.ads | |
../spec/has_value | ||
search_lower_bound_p.ads | ||
search_lower_bound_p.adb | ||
binary_search_p.ads | ||
binary_search_p.adb |