This directory contains the specification and implementation files
for the following algorithms: Max_Element, Max_Seq and
Min_Element. They are simple algorithms to find the max/min
element in an array.
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 |
|---|---|---|
| Max_Element | ../spec/upper_bound_p.ads | |
max_element_wo_ghost_p.ads | version without ghost function | |
max_element_wo_ghost_p.adb | ||
max_element_p.ads | version with ghost function | |
max_element_p.adb | ||
| Max_Seq | ../spec/has_value_p.ads | |
../spec/upper_bound_p.ads | ||
max_seq.ads | ||
max_sequence.adb | ||
| Min_Element | ../spec/lower_bound_p.ads | |
min_element_p.ads | ||
min_element_p.adb |