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.
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.
Sponsored by Ada-Europe