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:
2
Understanding program execution;
3
Reviewing object code;
4
Restricting language constructs whose
usage might complicate the demonstration of program correctness
4.1
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.
5
The pragmas
Reviewable and Restrictions relate to the other requirements addressed
by this Annex.
NOTES
6
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