This paper describes the design of ANNA (ANNotated ADA), a specification language for ADA programs. The project to design and implement ANNA, in progress at the time the paper was written, was being conducted by the author in collaboration with F. von Henke, B. Krieg-Brückner, and O. Owe.

The approach taken for specifying programs is based on that introduced by Hoare [1]. A program that is to perform a given task is annotated with a collection of assertions describing the state of program variables at various points in the program. These points include, at the minimum, the entry and exit points of each procedure and at least one point inside each loop. The assertions combine to state in an alternative manner what the program is supposed to be doing. Ultimately it is intended to verify the consistency between the code if the program and the assertions; proving this consistency is regarded as proving that the program is correctly performing the task implied by the assertions. However, even in the absence of the verification, the assertions are useful as explanatory material, e. g., as documentation to implementers and maintainers, as hints to the compiler for optimization opportunities, and as a specification for desired run-time checks that the assertions hold.

In fact, the emphasis of the paper is on these latter uses of the assertions. For example, in order to ensure that the program has the same end effect whether or not the assertions are evaluated at run time, the evaluated assertions are required not to have side effects.

ANNA is designed as an extension of ADA providing additional features useful for formal specification. The extensions are generalizations of existing explanatory constructs, e.g., constraints in declarations, new declarative constructs dealing with exceptions, context clauses and subprograms, and new specification constructs motivated by work in formal program specification, for specifying packages and composite types.

The assertions must be formal enough to be machine processable. Here the processing may range from mere syntactic checking, through arranging for run-time evaluation, to generating verification conditions for verifying consistency between the assertions and the executable code.

The programmer should be encouraged to actively use assertions in design, coding, and documentation. The semantics of the new features should be consistent with those already in ADA, and the extensions should be minimal.

ANNA follows the same scope rules as ADA. (This decision is odd given the complaint in the paper that the ADA scope rules are too permissive.) All assertions are expressed as ADA comments so that they can be ignored by a normal ADA processor. There are two kinds of assertions: virtual ADA text, in lines beginning with “--:”, and annotations, in lines beginning with “--|”. Virtual ADA text provides executable ADA statements that the annotations imagine to have been executed, e.g., to set ghost or history variables, but which are not executed when the unasserted program is run. The annotations provide assertions about the states of program variables.

Being able to write useful assertions requires some new operations and attributes including quantification, forall and exist, a new membership test is in (Section 2.3 promises explanation of the necessity of this new test in Section 2.4, but that explanation is found only in Section 3.2), and an attribute of access (pointer) types giving the collection of allocated objects referred to by values of the access type.

Among the annotations available for use are:

• (1)Object declaration annotations, providing constraints not normally expressible in ADA, e.g., subranges with holes.

• (2)Type and subtype declaration annotations, allowing the specification of a type or subtype not normally expressible in ADA, in terms of the set of values in them, e.g., the type of even integers; is in is used for testing membership in these types.

• (3)Statement annotations, describing the effect of a statement on program variables.

• (4)Subprogram annotations, describing the effect of a subprogram invocation as a function of its parameters.

• (5)Exception propagation annotations, which come in two flavors, strong and weak; a weak propagation annotation of a subprogram specifies exceptions that may be raised by a call to the subprogram; a strong propagation annotation of a subprogram specifies conditions of the in parameters under which an exception must be raised.

• (6)Package annotations, comprised of object, type, subprogram, and exception propagation annotations, describing the behavior of the visible identifiers of a package.