Derrick, J. and Boiten, E.A.
Refinement of objects and operations in Object-Z.
In: Smith, Scott F. and Talcott, Carolyn L., eds.
Fourth International Conference on Formal methods for open object-based distributed systems IV.
Kluwer Academic Publishers
ISBN 0-7923-7923-3 .
In this paper we describe how we can refine both objects and operations in an Object-Z specification. In particular, we will be concerned with changes of granularity of both objects and operations. Objects in that we wish to change the structure of objects in a specification. Operations in that we wish to provide explicit support for action refinement in this language. There are clear advantages in being able to change such levels of granularity when performing a refinement. In this paper we discuss the issues surrounding such refinements and derive general rules to support their use. We illustrate our ideas by looking at a specification of a cash point machine at a bank.
- Depositors only (login required):