ANNA: Towards a language for annotating Ada programs

ABSTRACT

ANNA is a proposal to extend Ada to include facilities for formally specifying the intended behaviour of Ada programs (or portions thereof) at all stages of program development. ANNA programs are Ada programs with formal comments. Formal comments in ANNA consist of virtul Ada text and annotations. The syntax and semantics of different kinds of annotations are defined: declarative annotations (for variables, subtypes, subprograms, and packages), statement annotations, exception annotations, and visibility annotations. ANNA includes a small number of predefined attributes which may appear only in annotations, e.g., access type collections. The lexical structure of ANNA is designed so that the extensions of Ada appear as Ada comments. ANNA programs are therefore acceptable by Ada translators. The semantics of annotations are defined in terms of Ada concepts, in particular many annotations are generalizations of the constraint concept. It is therefore a simple step for the Ada programmer to use ANNA to give formal specifications of programs. ANNA is intended to provide a formal framework within which different theories of formal specification may be applied to Ada. Our proposal omits tasking for the time being.

REFERENCES

• 1: Bauer, F.L., Broy, M., Gnatz, R., Hesse, W. and Krieg-Brückner, B., A Wide Spectrum Language for Program Development. In: Robinet, B. (ed.), Program Transformations: 3rd Int. Symp. on Programming, Paris (1978), 1-15.
• 2: Manfred Broy , Bernd Krieg-Bruckner, Derivation of Invariant Assertions During Program Development by Transformation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.321-337, July 1980 [doi>10.1145/357103.357108]
• 3: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 4: Hoare, C.A.R, and Wirth, N., An Axiomatic Definition of the Programming Language Pascal, Acta Informatica 2 (1973), 335-355.
• 5: J. D. Ichbiah, Preliminary Ada reference manual, ACM SIGPLAN Notices, v.14 n.6a, p.1-145, June 1979 [doi>10.1145/956650.956651]
• 6: Jean D. Ichbiah , Bernd Krieg-Brueckner , Brian A. Wichmann , John G. P. Barnes , Olivier Roubine , Jean-Claude Heliard, Rationale for the design of the Ada programming language, ACM SIGPLAN Notices, v.14 n.6b, p.1-261, June 1979 [doi>10.1145/956653.956654]
• 7: David C. Luckham , W. Polak, Ada exception handling: an axiomatic approach, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.2, p.225-233, April 1980 [doi>10.1145/357094.357100]
• 8: David C. Luckham , Wolfgang Polak, A practical method of documenting and verifying Ada programs with packages, Proceedings of the ACM-SIGPLAN symposium on The ADA programming language, p.113-122, January 1980 [doi>10.1145/800004.807941]
• 9: David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979 [doi>10.1145/357073.357078]
• 10: David C. Luckham , Steven M. German , Friedrich W. von Henke , Richard A. Karp , P. W. Milne , Derek C. Oppen , Wolfgang Polak , William L. Scherlis, Stanford Pascal Verifier user manual, Stanford University, Stanford, CA, 1979

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: ANNA

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Languages, Theory