This directory contains the specification and implementation files
for the following algorithms: Iota, Accumulate, Inner_Product,
Partial_Sum, Adjacent_difference and Numeric_Inv.
As usual, ghost functions used in specifications are
located in the spec directory at project root.
The algorithms presented in this chapter do not introduce any real difficulties when proving them, except for one point: the absence of overflow issues during computations.
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 |
|---|---|---|
| Iota | ../spec/is_iota_p.ads | |
iota_p.ads | ||
iota_p.adb | ||
| Accumulate | ../spec/acc_def_naive_p.ads | |
accumulate_naive_p.ads | naive implementation without proper overflow handling | |
accumulate_naive_p.adb | ||
../spec/acc_def_p.ads | ||
../spec/overflow.ads | ||
accumulate_p.ads | correct implementation with proper overflow handling | |
accumulate_p.adb | ||
| Inner_Product | ../spec/inner_prod_def_p.ads | |
../spec/overflow.ads | ||
inner_product_p.ads | ||
inner_product_p.adb | ||
| Partial_Sum | ../spec/acc_def_p.ads | |
../spec/overflow.ads | ||
partial_sum_p.ads | ||
partial_sum_p.adb | ||
| Adjacent_Difference | ../spec/overflow.ads | |
adjacent_difference_p.ads | ||
adjacent_difference_p.adb | ||
| Numeric_Inv | ../spec/acc_def_p.ads | |
../spec/overflow.ads | ||
adjacent_difference_p.ads | ||
adjacent_difference_p.adb | ||
partial_sum_p.ads | ||
partial_sum_p.adb | ||
numeric_inv.ads | ||
numeric_inv.adb |