Refinement of objects and operations in Object-Z

Derrick, John and Boiten, Eerke (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 . (Full text available)

Postscript
Download (234kB)
[img]
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: 13 May 2014 08:32
Resource URI: http://kar.kent.ac.uk/id/eprint/21969 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year