School of Computing

A Case Study in Partial Specification: Consistency and Refinement for Object-Z

Chris Taylor, John Derrick, and Eerke Boiten

In Proc. of ICFEM 2000, pages 182-196. IEEE, September 2000.


The `viewpoint' approach, in which a system is described by several partial specifications, has been proposed as a way of making complex computing systems more understandable. The ISO's Open Distributing Processing (ODP) framework is an architecture for open distributed systems, involving five named viewpoints. This paper compares two partial specifications of a lending library --- from the ODP's Enterprise and Information Viewpoints --- and discusses the relation between them. Both specifications are written in Object-Z, an object-oriented variant of Z. Examining how such partial specifications might be unified raises broader issues of refinement and mutual consistency of partial specifications in Object-Z.

Bibtex Record

author = {Chris Taylor and John Derrick and Eerke Boiten},
title = {A {C}ase {S}tudy in {P}artial {S}pecification: {C}onsistency and {R}efinement for {O}bject-{Z}},
month = {September},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    booktitle = {Proc. of ICFEM 2000},
    organization = {IEEE},
    publication_type = {inproceedings},
    refereed = {yes},
    submission_id = {13702_963490791},

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

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

Last Updated: 21/03/2014