Issues in the Refinement of Distributed Programs

Abstract

Developing correct computer programs is a notoriously difficult task, which has attracted a significant intellectual effort over the past decades. One attractive methodology that has been proposed to tackle this problem consists of systems for program refinement, in which a calculus is given for transforming, often in a top-down manner, the specification of a computational task into a program implementing this specification (excellent introductions to refinement are Back and von Wright 1998 and Morgan 1994). Calculi for the refinement of sequential programs are by now a mature and well-established field. In this abstract, I wish to discuss some issues that arise when we try to develop a refinement calculus for distributed programs. This discussion is based on a joint project with Ron van der Meyden and Kai Engelhardt of the University of New South Wales, Sydney, Australia. Some insight into the technical aspects of the approach we are pursuing can be found in Engelhardt et al. 1998 and 2000 and in van der Meyden and Moses 2000.1 An obvious point to start a discussion of refinement for distributed programs is the sequential case. The subtlety and inherent complexity of distributed systems make the task of refinement for distributed programs much harder. The purpose of this abstract is to discuss, in an informal fashion, some of the distinctive issues that seem to play a role in this effort. The hope is that a discussion of these issues may contribute to other work on formal and algorithmic approaches to distributed computation.

Insights described here have been obtained as part of this joint work; any mistakes or misrepresentations are my own doing.