This reference manual of ANNA is another volume addressed to the ADA
community. ANNA is a language extension of ADA to include facilities for
formally specifying the intended behavior of ADA programs. It is
designed to meet a perceived need to augment ADA with precise
machine-processable annotations so that well established formal methods
of specification and documentation can be applied to ADA programs. The
current ANNA design includes annotations of all ADA constructs except
tasking. Similar extensions for formal specification can be made to
other Algol-like languages such as Pascal, PL/1, Concurrent Pascal, and
Modula; essentially, these extensions would be subsets of ANNA. The
design of ANNA was undertaken from the beginning with four principal
considerations: 1. Constructing annotations should be easy for the ADA
programmer and should depend as much as possible on notation and
concepts of ADA. 2. ANNA should possess language features that are
widely used in the specification and documentation of programs. 3. ANNA
should provide a framework within which the various established theories
of formally specifying programs may be applied to ADA. 4. Annotations
should be equally well suited for different possible applications during
the life cycle of a program. Such applications include not only testing,
debugging and formal verification of a finished program, but also
specification of program parts during the earlier stages of requirements
analysis and program design.
