Comparison of Data and Process Refinement

Abstract

From what point of view is it reasonable, or possible, to refine a one place buffer into a two place buffer? In order to answer this question we characterise refinement based on substitution in restricted contexts. We see that data refinement (specifically in Z) and process refinement give differing answers to the original question, and we compare the precise circumstances which give rise to this difference by translating programs and processes into labelled transition systems, so providing a common basis upon which to make the comparison. We also look at the closely related area of sub-typing of objects. Along the way we see how all these sorts of computational construct are related as far as refinement is concerned, and discover and characterise some (as far as we can tell) new sorts of refinement. Keywords: data refinement, process refinement, labelled transition systems, Z, sub-typing. © Springer-Verlag 2003.