ANNA is an acronym for annotated Ada.
Annotated Ada is a high-level programming language that extends Ada with various kinds of specification constructs. The language includes special annotating constructs, or semantic assertions, that lay down axioms about the procedures and other facilities of the Ada program.
ANNA is based on first-order logic and includes generalized type constraints, virtual checking functions and behavior specification constructs, from simple assertions to complex algebraic specifications.
