Refinement in Z and Object-Z

I. Refining Z Specifications.- 1. An Introduction to Z.- 1.1 Z: A Language for Specifying Systems.- 1.2 Predicate Logic and Set Theory.- 1.3 Types, Declarations and Abbreviations.- 1.3.1 Types.- 1.3.2 Axiomatic Definitions.- 1.3.3 Abbreviations.- 1.4 Relations, Functions, Sequences and Bags.- 1.4.1 Relation.- 1.4.2 Functions.- 1.4.3 Sequences.- 1.4.4 Bags.- 1.5 Schemas.- 1.5.1 Schema Syntax.- 1.5.2 Schema Inclusion.- 1.5.3 Decorations and Conventions.- 1.5.4 States, Operations and ADTs.- 1.5.5 The Schema Calculus.- 1.5.6 Schemas as Declarations.- 1.5.7 Schemas as Predicates.- 1.5.8 Schemas as Types.- 1.5.9 Schema Equality.- 1.6 An Example Refinement.- 1.7 What Does a Z Specification Mean?.- 1.8 The Z Standard.- 1.9 Tool Support.- 1.10 Bibliographical Notes.- 2. Simple Refinement.- 2.1 What is Refinement?.- 2.2 Operation Refinement.- 2.3 From Concrete to Abstract Data Types.- 2.4 Establishing and Imposing Invariants.- 2.4.1 Establishing Invariants.- 2.4.2 Imposing Invariants.- 2.5 Example: London Underground.- 2.6 Bibliographical Notes.- 3. Data Refinement and Simulations.- 3.1 Programs and Observations for ADTs.- 3.2 Upward and Downward Simulations.- 3.3 Dealing with Partial Relations.- 3.4 Bibliographical Notes.- 4. Refinement in Z.- 4.1 The Relational Basis of a Z Specification.- 4.2 Deriving Downward Simulation in Z.- 4.3 Deriving Upward Simulation in Z.- 4.4 Embedding Inputs and Outputs.- 4.5 Deriving Simulation Rules in Z - Again.- 4.6 Examples.- 4.7 Reflections on the Embedding.- 4.7.1 Alternative Embeddings.- 4.7.2 Programs, Revisited.- 4.8 Proving and Disproving Refinement.- 4.9 A Pitfall: Name Capture.- 4.10 Bibliographical Notes.- 5. Calculating Refinements.- 5.1 Downward Simulations.- 5.1.1 Non-Functional Retrieve Relations.- 5.2 Upward Simulations.- 5.3 Calculating Common Refinements.- 5.4 Bibliographical Notes.- 6. Promotion.- 6.1 Example: Multiple Processors.- 6.2 Example: A Football League.- 6.3 Free Promotions and Preconditions.- 6.4 The Refinement of a Promotion.- 6.4.1 Example: Refining Multiple Processors.- 6.4.2 Refinement Conditions for Promotion.- 6.5 Commonly Occurring Promotions.- 6.6 Calculating Refinements.- 6.7 Upward Simulations of Promotions.- 6.8 Bibliographical Notes.- 7. Testing and Refinement.- 7.1 Deriving Tests from Specifications.- 7.2 Testing Refinements and Implementations.- 7.2.1 Calculating Concrete Tests.- 7.2.2 Calculating Concrete States.- 7.3 Building the Concrete Finite State Machine.- 7.3.1 Using a Functional Retrieve Relation.- 7.3.2 Using a Non-Functional Retrieve Relation.- 7.4 Refinements due to Upward Simulations.- 7.5 Bibliographical Notes.- 8. A Single Simulation Rule.- 8.1 Powersimulations.- 8.2 Appfication to Z.- 8.3 Calculating Powersimulations.- 8.4 Bibliographical Notes.- II. Interfaces and Operations: ADTs Viewed in an Environment.- 9. Refinement, Observation and Modification.- 9.1 Grey Box Data Types.- 9.2 Refinement of Grey Box Data Types.- 9.3 Display Boxes.- 9.4 Bibliographical Notes.- 10. IO Refinement.- 10.1 Examples of IO Refinement: "Safe" and "Unsafe"..- 10.2 An Embedding for IO Refinement.- 10.3 Intermezzo: IO Transformers.- 10.4 Deriving IO Refinement.- 10.4.1 Initialisation.- 10.4.2 Finalisation.- 10.4.3 Applicability.- 10.4.4 Correctness.- 10.5 Conditions of IO Refinement.- 10.6 Further Examples.- 10.7 Bibliographical Notes.- 11. Weak Refinement.- 11.1 Using Stuttering Steps.- 11.2 Weak Refinement.- 11.2.1 The Relational Context.- 11.2.2 The Schema Calculus Context.- 11.2.3 Further Examples.- 11.3 Properties.- 11.3.1 Weak Refinement is Not a Pre-Congruence.- 11.3.2 Internal Operations with Output.- 11.4 Upward Simulations.- 11.5 Removing Internal Operations.- 11.6 Divergence.- 11.7 Bibhographical Notes.- 12. Non-Atomic Refinement.- 12.1 Non-Atomic Refinement via Stuttering Steps.- 12.1.1 Semantic Considerations.- 12.1.2 Using the Schema Calculus.- 12.2 Non-Atomic Refinement Without Stuttering.- 12.3 Using IO Transformations.- 12.3.1 Semantic Considerations Again.- 12.3.2 The Z Characterisation.- 12.4 Further Examples.- 12.5 Varying the Length of the Decomposition.- 12.6 Upward Simulations.- 12.7 Properties and Discussion.- 12.7.1 Non-interference.- 12.7.2 Interruptive.- 12.7.3 Interleaving.- 12.7.4 Further Non-Atomic Refinements.- 12.8 Bibliographical Notes.- 13. Case Study: A Digital and Analogue Watch.- 13.1 The Abstract Design.- 13.2 Grey Box Specification and Refinement.- 13.3 An Analogue Watch: Using IO Refinement.- 13.4 Adding Seconds: Weak Refinement.- 13.5 Resetting the Time: Using Non-Atomic Refinement.- 14. Further Generalisations.- 14.1 Alphabet Extension.- 14.2 Alphabet Translation.- 14.3 Compatibility of Generalisations.- 14.4 Bibliographical Notes.- III. Object-Oriented Refinement.- 15. An Introduction to Object-Z.- 15.1 Classes.- 15.1.1 The Object-Z Schema Calculus.- 15.1.2 Late Binding of Operations.- 15.1.3 Preconditions.- 15.2 Inheritance.- 15.2.1 Example: A Bank Account.- 15.3 Object Instantiation.- 15.3.1 Modelling Aggregates.- 15.3.2 Example: A Bank.- 15.3.3 Object Containment.- 15.4 Communicating Objects.- 15.5 Semantics.- 15.5.1 Polymorphism and Generic Parameters.- 15.6 Example: A Football League.- 15.7 Bibliographical Notes.- 16. Refinement in Object-Z.- 16.1 The Simulation Rules in Object-Z.- 16.2 Weak Refinement in Object-Z.- 16.3 Grey Box, IO, and Non-Atomic Refinement in Object-Z.- 16.3.1 Non-Atomic Refinement.- 16.4 Refinement, Subtyping and Inheritance.- 16.5 Bibliographical Notes.- 17. Class Refinement.- 17.1 Objects and References.- 17.1.1 Understanding Object Evolution.- 17.1.2 Verifying the Bank Refinement.- 17.2 Class Simulations.- 17.3 Issues of Compositionality.- 17.3.1 Promoting Refinements Between Object-Z Classes.- 17.4 Bibliographical Notes.- IV. Modelling State and Behaviour.- 18. Combining CSF and Object-Z.- 18.1 An Introduction to CSP.- 18.1.1 The Semantics of CSP.- 18.2 Integrating CSP and Object-Z.- 18.2.1 A Common Semantic Model.- 18.3 Combining CSP Processes and Object-Z Classes.- 18.4 Combining Object-Z Classes using CSP Operators.- 18.5 Bibliographical Notes.- 19. Refining CSP and Object-Z Specifications.- 19.1 Refinement in CSP.- 19.1.1 Using Simulations with CSP Refinement.- 19.2 Refinement of CSP Components.- 19.3 Refinement of Object-Z Components.- 19.3.1 Example: The Lift Specification.- 19.4 Structural Refinements.- 19.5 Bibliographical Notes.- 20. Conclusions.- Glossary of Notation.