Ada 2012 Reference Manual
Annex H
(normative)
High Integrity Systems
This Annex addresses requirements for high integrity systems (including safety-critical systems and security-critical systems). It provides facilities and specifies documentation requirements that relate to several needs:
- Understanding program execution;
- Reviewing object code;
- Restricting language constructs whose usage might complicate the demonstration of program correctness
Execution understandability is supported by pragma Normalize_Scalars, and also by requirements for the implementation to document the effect of a program in the presence of a bounded error or where the language rules leave the effect unspecified.
The pragmas Reviewable and Restrictions relate to the other requirements addressed by this Annex.
NOTES
1 The Valid attribute (see 13.9.2) is also useful in addressing these needs, to avoid problems that could otherwise arise from scalars that have values outside their declared range constraints.
