Refinement in Z and Object-Z

Part I. Refining Z Specifications

1. An Introduction to Z
John Derrick, Eerke A. Boiten

2. Simple Refinement
John Derrick, Eerke A. Boiten

3. Data Refinement and Simulations
John Derrick, Eerke A. Boiten

4. Refinement in Z
John Derrick, Eerke A. Boiten

5. Calculating Refinements
John Derrick, Eerke A. Boiten

6. Promotion
John Derrick, Eerke A. Boiten

7. Testing and Refinement
John Derrick, Eerke A. Boiten

8. A Single Simulation Rule
John Derrick, Eerke A. Boiten

Part II. Interfaces and Operations: ADTs Viewed in an Environment

9. Refinement, Observation and Modification
John Derrick, Eerke A. Boiten

10. IO Refinement
John Derrick, Eerke A. Boiten

11. Weak Refinement
John Derrick, Eerke A. Boiten

12. Non-atomic Refinement
John Derrick, Eerke A. Boiten

13. Case Study: A Digital and Analogue Watch
John Derrick, Eerke A. Boiten

14. Further Generalisations
John Derrick, Eerke A. Boiten

Part III. Object-Oriented Refinement

15. An Introduction to Object-Z
John Derrick, Eerke A. Boiten

16. Refinement in Object-Z
John Derrick, Eerke A. Boiten

17. Class Refinement
John Derrick, Eerke A. Boiten

Part IV. Modelling State and Behaviour

18. Combining CSP and Object-Z
John Derrick, Eerke A. Boiten

19. Refining CSP and Object-Z Specifications
John Derrick, Eerke A. Boiten

20. Conclusions
John Derrick, Eerke A. Boiten

Nyckelord: Computer Science, Mathematical Logic and Formal Languages, Software Engineering