Format:
1 Online-Ressource (xvi, 335 pages)
,
digital, PDF file(s)
ISBN:
9780511569777
Series Statement:
Cambridge tracts in theoretical computer science 35
Content:
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
Content:
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
Content:
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
Content:
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
Note:
Title from publisher's bibliographic system (viewed on 05 Oct 2015)
Additional Edition:
ISBN 9780521434577
Additional Edition:
ISBN 9780521435925
Additional Edition:
Erscheint auch als Druck-Ausgabe ISBN 9780521434577
Language:
English
DOI:
10.1017/CBO9780511569777
Bookmarklink
