David Luckham

Programming with Specifications (eBook, PDF)

An Introduction to ANNA, A Language for Specifying Ada Programs

• Format: PDF

Produktbeschreibung

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

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer US
• Seitenzahl: 416
• Erscheinungstermin: 6. Dezember 2012
• Englisch
• ISBN-13: 9781461396857
• Artikelnr.: 44176585

Inhaltsangabe

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.