Refinement in Z and Object-Z: Foundations and Advanced Applications - Softcover

Inhaltsangabe

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

Die Inhaltsangabe kann sich auf eine andere Ausgabe dieses Titels beziehen.