Programming with Specifications

Topics - what this book is about, - its intended audience, - what the reader ought to know, - how the book is organized, - acknowledgements. Specifications express information about a program that is not normally part of the program, and often cannot be expressed in a programming lan guage. In the past, the word "specification" has sometimes been used to refer to somewhat vague documentation written in English. But today it indicates a precise statement, written in a machine processable language, about the purpose and behavior of a program. Specifications are written in languages that are just as precise as programming languages, but have additional capabilities that increase their power of expression. The termi nology formal specification is sometimes used to emphasize the modern meaning. For us, all specifications are formal. The use of specifications as an integral part of a program opens up a whole new area of programming - progmmming with specifications. This book describes how to use specifications in the process of building programs, debugging them, and interfacing them with other programs. It deals with a new trend in programming - the evolution of specification languages from the current generation of programming languages. And it describes new strategies and styles of programming that utilize specifications. The trend is just beginning, and the reader, having finished this book, will viii Preface certainly see that there is much yet to be done and to be discovered about programming with specifications.

Inhalt
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 Rigo