0 What Anna Is. - 0. 1 From Informal Comments to Formal Annotations. - 0. 2 Adding Annotations to Ada. - 0. 3 Applying Anna. - 0. 4 Environments for Programming with Specifications. - 0. 5 Future Developments. - 0. 6 Terminology and Notation. - 1 Simple Annotations. - 1. 1 Annotations. - 1. 2 The Meaning of Simple Annotations. - 1. 3 Anna Expressions. - 1. 4 Quantified Expressions. - 1. 5 Modifiers. - 1. 6 Assertions. - 1. 7 Compound Statement Annotations. - 1. 8 Object Annotations. - 1. 9 Subprogram Annotations. - 1. 10 Type Annotations. - 1. 11 Elaboration of Annotations. - 1. 12 Proper Annotations. - 2 Using Simple Annotations. - 2. 1 Three General Activities. - 2. 2 Virtual Text. - 2. 3 Assertions as Tests and Documentation. - 2. 4 Assertions and Timing. - 2. 5 Assertions in Loops. - 2. 6 Invariants: Compound Statement Annotations. - 2. 7 Increasing the Scope of Annotations. - 2. 8 Specification Using Subprogram Annotations. - 2. 9 Runtime Checking of Simple Annotations. - 3 Exceptions. - 3. 1 Annotating Raising and Handling of Exceptions. - 3. 2 Propagation Annotations. - 3. 3 Annotating Exception Propagation. - 4 Package Specifications. - 4. 1 Annotations and Package Structure. - 4. 2 Simple Annotations in Package Declarations. - 4. 3 Package States. - 4. 4 Using Package States. - 4. 5 Package Axioms. - 4. 6 Restrictions on Package States. - 5 The Process of Specifying Packages. - 5. 1 Getting Started. - 5. 2 Theory Packages. - 5. 3 A PL/1 String Manipulation Package. - 5. 4 A Simple Sets Package. - 5. 5 Dependent Specification. - 5. 6 Relative Specification. - 5. 7 The DIRECT_IO Package. - 5. 8 Symbolic Execution of Specifications. - 5. 9 Iterators and Generators. - 6 Annotation of Generic Units. - 6. 1 Generic Annotations. - 6. 2 Generic Parameter Constraints. - 6. 3 Annotated Generic Units as Reusable Software. - 7 Annotation of Operations on Composite Types. - 7. 1 Array States. - 7. 2 Using Array States: QuickSort. - 7. 3 Record States. - 7. 4 Access Types and Collections. - 7. 5 Using Collections. - 8 Annotation of the Hidden Parts of Packages. - 8. 1 Modified Type Annotations. - 8. 2 Representation of Package States. - 8. 3 Annotation of Hidden Package States. - 8. 4 Annotation of Package Subprogram Bodies. - 8. 5 Establishing Consistency. - 8. 6 Redefinition of Equality. - 8. 7 Packages as Types. - 9 Interpretation of Package Specifications *. - 9. 1 Why Interpretations Are Useful. - 9. 2 Constructing Interpretations. - 9. 3 Interpreting Subprogram Annotations. - 9. 4 Full Specifications of Subprogram Bodies. - 9. 5 Interpreting Package Axioms. - 9. 6 Interpreting Dependent Specifications. - 10 Processes for Consistent Implementation of Packages. - 10. 1 Making the Normal Ada Process More Rigorous. - 10. 2 A Process Based on Runtime Checking. - 10. 3 A Rigorous Process Based on Consistency Proof. - 10. 4 An Example: Implementing a Package Body. - A Syntax. - B Tools. - B. 1 The Anna Runtime Checking System. - B. 2 Package Specification Analyzer. - C A Short Bibliography. - C. 1 Anna. - C. 2 Ada. - C. 3 Specification Languages. - C. 4 Formal Methods. - C. 5 Testing. Language: English