Title from publisher's bibliographic system (viewed on 05 Oct 2015).
3.7. Semantics of normal-form specifications. 3.8. Hidden names. 4. Implementing algebraic specifications. 4.2. Expressions. 4.3. Term interpretation of expressions. 4.4. Declarations. 4.5. Survey of assertions and expressions. 4.6. Algorithmic predicate definitions. 4.7. Algorithmic function definitions. 4.8. From inductive to algorithmic definitions. 4.9. Implementing an algebraic specification. 4.10. Example: implementation of sets -- II. State-based specification. 5. From algebras to states. 5.2. What is a state-based specification? 5.3. Procedure names and class signatures. 5.4. States as algebras. 5.5. Classes. 5.6. Introducing variables. 5.7. Procedure definitions. 5.8. Comparison with imperative programs. 5.9. From predicate logic to dynamic logic. 5.10. Classes and specifications. 6. Setting up state-based specifications. 6.1. Kinds of axioms. 8.7. Example: implementation of a line editor. 8.7.1. Specifying the system. 8.7.2. Documenting a building block. 8.7.3. Choosing a representation. 8.7.4. Adding display-oriented features. 8.7.5. Implementing the display-oriented features. 8.7.6. Translation to C. 8.7.7. Executing the program -- III. Advanced techniques. 9. Theoretical topics. 9.2. Undefinedness revisited. 9.3. Initial algebras. 9.4. Horn clauses. 9.5. Origin consistency. 9.6. Comparing two types of models. 9.7. The class concept revisited. 10. Additional language constructs. 10.2. Liberal scope rules. 10.3. Free definitions. 10.4. Parameterisation. 10.5. Abstraction schemes. 10.6. Application schemes. 10.7. Extending the normalization procedure. 10.8. More complex parameter restrictions. 10.9. Object creation and procedures with results. 10.10. Variable sort definitions. 10.11. Dependent definitions. 10.12. Example: specification of instances. 10.13. Unifying expressions and statements. 11. Towards large systems. 11.2. Graphical representation of modules. 11.3. Components and designs. 11.4. Applications. 11.5. Concluding remarks -- A Syntax. A.1 General. A.2 Concrete syntax. A.3 Tokens. A.4 Keywords. A.5 Comments. A.6 Grammar. A.7 Operator priorities and associativities. A.7.1 Operators in renamings and signatures. A.7.2 Operators in assertions and expressions -- B Standard library. B.1 Booleans. B.2 Natural numbers. B.3 Characters. B.4 Tuples. B.5 Finite sets. B.6 Finite bags. B.7 Finite sequences. B.8 Finite maps.
Formal specification is a method for precisely modelling computer-based systems that combines concepts from software engineering and mathematical logic. In this book the authors describe algebraic and state-based specification techniques from the unified view of the Common Object-oriented Language for Design, COLD, a wide-spectrum language in the tradition of VDM and Z. The kernel language is explained in detail, with many examples, including: set representation, a display device, an INGRES-like database system, and a line editor. Fundamental techniques such as initial algebra semantics, loose semantics, partial functions, hiding, sharing, predicate and dynamic logic, abstraction functions, representation of invariants and black-box correctness are also presented. More advanced ideas, for example Horn logic, and large systems are given in the final part. Appendices contain full details of the language's syntax and a specification library. Techniques for software development and design are emphasised throughout, so the book will be an excellent choice for courses in these areas.