language: en

On the Relation Between Unity Properties and Sequences of States

R.T. Udink
Utrecht University, Department of Computer Science,
P.O. Box 80.089, 3508 TB Utrecht, the Netherlands
J.N. Kok
Utrecht University, Department of Computer Science,
P.O. Box 80.089, 3508 TB Utrecht, the Netherlands

ABSTRACT Stepwise refinement of programs has proven to be a suitable method for developing parallel and distributed programs. We examine and compare a number of different notions of program refinement for Unity. Two of these notions are based on execution sequences. Refinement corresponds to the reduction of the set of execution sequences, i.e. reducing the amount of nondeterminism. The other refinement notions are based on Unity properties as introduced by Chandy and Misra. The Unity approach is to refine specifications. Although it has proven a suitable formalism for deriving algorithms, it seems less suitable for handling implementation details. Following Sanders and Singh, we formalize program refinement in the Unity framework as the preservation of Unity properties. We show that Unity properties are not powerful enough to characterize execution sequences. As a consequence, the notion of property-preserving refinement differs from the notion of reducing the set of execution sequences.

Keywords Semantic models, Unity, program refinement.

CONTENTS 0 Introduction