Report Number: CSL-TR-84-261
Institution: Stanford University, Computer Systems Laboratory
Title: ANNA: a language for annotating ADA programs
Author: Luckham, David C.
Author: Henke, Friedrich W. von
Author: Krieg-Brueckner, Bernd
Author: Owe, Olaf
Date: July 1984
Abstract: ANNA is a proposed language extension of Ada to include facilities for formally specifying the intended behavior of Ada programs (or portions thereof) at all stages of program development. Anna programs are Ada programs extended by formal comments. Formal comments in ANNA consist of virtual Ada text and annotations. Anna provides annotations for all Ada constructs, including declarative annotations (for variables, subtypes, subprograms, and packages), statement annotations, annotations of generic units, exception annotations and visibility annotations. (The current Anna design does not include extensions for annotating Ada multi-tasking constructs.) Anna also includes a small number of new predefined attributes, which may appear only in annotations, e.g. the collection attribute of an access type. Since all Anna extensions appear as Ada comments, Anna programs are also legal Ada programs and acceptable by Ada translators. The semantics of annotations are defined in terms of Ada concepts; in particular, many kinds of annotations are generalizations of the Ada constraint concept. This simplifies the training of Ada programmers to use Anna for formal specification of Ada programs. Anna provides a formal framework within which different theories of formal specification may be applied to Ada. This manual also describes a translation of annotations into Ada text for run-time check of consistency with annotations.
http://i.stanford.edu/pub/cstr/reports/csl/tr/84/261/CSL-TR-84-261.pdf