Programming with Specifications : An Introduction to ANNA, A Language for Specifying Ada Programs

This monograph introduces ANNA, a language for specifying programs written in Ada.

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.9.1 Out values of procedure parameters.- 1.9.2 Conformance of subprogram annotations.- 1.10 Type Annotations.- 1.10.1 Anna membership test.- 1.11 Elaboration of Annotations.- 1.12 Proper Annotations.- 2 Using Simple Annotations.- 2.1 Three General Activities.- 2.2 Virtual Text.- 2.2.1 Formalizing concepts.- 2.2.2 Rules for virtual text.- 2.3 Assertions as Tests and Documentation.- 2.3.1 Choosing assertions.- 2.3.2 When to use assertions to express tests.- 2.4 Assertions and Timing.- 2.5 Assertions in Loops.- 2.5.1 Successor functions.- 2.5.2 Related assertions.- 2.5.3 Structuring testing and proof.- 2.5.4 Loop induction.- 2.6 Invariants: Compound Statement Annotations.- 2.7 Increasing the Scope of Annotations.- 2.8 Specification Using Subprogram Annotations.- 2.8.1 Specifying subprograms.- 2.8.2 Formalizing and organizing concepts.- 2.9 Runtime Checking of Simple Annotations.- 3 Exceptions.- 3.1 Annotating Raising and Handling of Exceptions.- 3.1.1 Consistency of raising and handling 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.4.1 Evaluating package functions in a state.- 4.4.2 Successor states.- 4.4.3 Equality on state types.- 4.5 Package Axioms.- 4.5.1 Axioms for equality.- 4.6 Restrictions on Package States.- 4.6.1 Restrictions on use of state attributes.- 4.6.2 State attributes of generic packages.- 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.6.1 Extension.- 5.6.2 Association―Modeling types with other types.- 5.6.3 An example of relative specification by association ― Small Library.- 5.7 The DIRECT_IO Package.- 5.8 Symbolic Execution of Specifications.- 5.8.1 A recipe for symbolic execution.- 5.8.2 An example of symbolic execution.- 5.9 Iterators and Generators.- 6 Annotation of Generic Units.- 6.1 Generic Annotations.- 6.2 Generic Parameter Constraints.- 6.2.1 Rationale for restricting generic parameter annotations.- 6.3 Annotated Generic Units as Reusable Software.- 6.3.1 Generalization.- 6.3.2 Specifying generic contexts.- 6.3.3 Generic theories.- 7 Annotation of Operations on Composite Types.- 7.1 Array States.- 7.2 Using Array States: QuickSort.- 7.3 Record States.- 7.3.1 Variant record states.- 7.4 Access Types and Collections.- 7.4.1 Collections.- 7.4.2 Collection states and operations.- 7.5 Using Collections.- 8 Annotation of the Hidden Parts of Packages.- 8.1 Modified Type Annotations.- 8.1.1 Stability constraints.- 8.1.2 Changing values of composite types.- 8.1.3 Semantics of modified type annotations.- 8.2 Representation of Package States.- 8.2.1 Restrictions on using package states.- 8.2.2 Hidden state property.- 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.