Research Repository

CSM-362a - An Analysis of total correctness refinement models for partial relation semantics I

Henson, M and Reeves, S (2002) CSM-362a - An Analysis of total correctness refinement models for partial relation semantics I. UNSPECIFIED. CSM-362a, University of Essex, Colchester.

[img]
Preview
Text
csm-362a.PDF - Other

Download (2MB) | Preview

Abstract

This is the first of a series of papers devoted to the thorough investigation of (total correctness) refinement based on an underlying partial relational model. In this paper we restrict attention to operation refinement. We explore four theories of refinement based on an underlying partial relation model for specifications, and we show that they are all equivalent. This, in particular, sheds some light on the relational completion operator (lifted-totalisation) due to Woodcock which underlies data refinement in, for example, the specification language Z. It further leads to two simple alternative models which are also equivalent to the others.

Item Type: Monograph (UNSPECIFIED)
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: Faculty of Science and Health > Computer Science and Electronic Engineering, School of
Depositing User: Julie Poole
Date Deposited: 27 Feb 2014 11:51
Last Modified: 17 Aug 2017 17:54
URI: http://repository.essex.ac.uk/id/eprint/8669

Actions (login required)

View Item View Item