Derrick / Boiten Refinement in Z and Object-Z

Foundations and Advanced Applications
2001
ISBN: 978-1-4471-0257-1
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 466 Seiten, eBook

Reihe: Formal Approaches to Computing and Information Technology (FACIT)

Refinement is one of the cornerstones of the formal approach to software engineering, and its use in various domains has led to research on new applications and generalisation. This book brings together this important research in one volume, with the addition of examples drawn from different application areas. It covers four main themes:
- data refinement and its application to Z;
- generalisations of refinement that change the interface and atomicity of operations;
- refinement in Object-Z;
- and modelling state and behaviour by combining Object-Z with CSP.
Refinement in Z and Object-Z: Foundations and Advanced Applications provides an invaluable overview of recent research for academic and industrial researchers, lecturers teaching formal specification and development, industrial practitioners using formal methods in their work, and postgraduate and advanced undergraduate students.

Zielgruppe

Research

Autoren/Hrsg.

Derrick, John

Boiten, Eerke A.

Inhaltsverzeichnis

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.