School of Computing

Refinement of objects and operations in Object-Z

John Derrick and Eerke Boiten

In Scott F. Smith and Carolyn L. Talcott, editors, Formal Methods for Open Object-based Distributed Systems IV, pages 182-196. Kluwer Academic Publishers, September 2000.

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.

Download publication 228 kbytes (PostScript)

Bibtex Record

@inproceedings{1120,
author = {John Derrick and Eerke Boiten},
title = {Refinement of objects and operations in {O}bject-{Z}},
month = {September},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/1120},
    booktitle = {Formal Methods for Open Object-based Distributed Systems IV},
    editor = {Scott F. Smith and Carolyn L. Talcott},
    publication_type = {inproceedings},
    publisher = {Kluwer Academic Publishers},
    refereed = {yes},
    submission_id = {19688_969029559},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014