Programming with Specifications

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.