DocAda^(tm) is a productivity tool of KSCE

| | | |
About DocAda Light: Preface / Preliminary / Help / TOC / Copyright
DocAda Online at the Ada Home: Complete RM95 / Updates / News

Annex H: Safety and Security
(normative)

This Annex addresses requirements for systems that are safety critical or have security constraints. 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.

Clauses and Subclauses

1. Pragma Normalize_Scalars
2. Documentation of Implementation Decisions
3. Reviewable Object Code
   1. Pragma Reviewable
   2. Pragma Inspection_Point
4. Safety and Security Restrictions

About DocAda Light: Preface / Preliminary / Help / TOC / Copyright
DocAda Online at the Ada Home: Complete RM95 / Updates / News
| | | |