Refinement of objects and operations in Object-Z

Derrick, J. and Boiten, E.A. (2000) 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 pp. 257-277. ISBN 0-7923-7923-3 .

Postscript
Download (228Kb)	Preview

Abstract

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.

Item Type:	Conference or workshop item (Paper)
Uncontrolled keywords:	Object-Z; refinement; action refinement; object structure
Subjects:	Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions:	Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User:	Mark Wheadon
Date Deposited:	12 Sep 2009 15:40
Last Modified:	12 Jun 2012 12:55
Resource URI:	http://kar.kent.ac.uk/id/eprint/21969 (The current URI for this page, for reference purposes)

• Depositors only (login required):