Program refinement in UNITY

Abstract

Program refinement has received a lot of attention in the context of stepwise development of correct programs, since the introduction of transformational programming techniques by [Wir71, Hoa72, Ger75, BD77] in the seventies. This report presents a new framework of program refinement, that is based on a refinement relation between UNITY programs. The main objective of introducing this new relation it to reduce the complexity of correctness proofs for existing classes of related distributed algorithms. It is shown, however, that this relation is also suitable for the stepwise development of programs, and incorporates most of the program transformations found in existing work on refinements.