ANNA. A language for annotating Ada programs. Reference manual (Q578891)

Anna is an extension of Ada. An Anna program consists of an Ada program supplied with formal comments of two kinds: virtual Ada text and annotations. A virtual text is presented by means of Ada constructs. It defines concepts used in annotations. The purpose of annotations is to specify the intended behavior of Ada programs by means of Boolean relationships between program variables. The annotations must be described by constructs defined in Anna language. The Anna syntax is an extension of the Ada syntax. The Ada expressions are extended by logical quantifiers. The book is structured in the same way as the Ada Programming Language Reference Manual. Thus it is convenient to use both books together. There are described the annotations of all constructs of Ada such as declarations, types, statements, subprograms packages, compilation units, exceptions, generic units, etc. with the exception of tasks (``A theory of annotations of tasks and multitask systems has yet to be developed. Extensions of Anna to tasks are planned'' - is said by the authors of the book). The Anna kernel subset is used to describe the semantics of Anna.