On the design and specification of message oriented programs

Processes are building blocks for the modeling of environments in which parallel and distributed processing occurs. In parallel programming they play the role of standard units (as do subroutines or procedures in sequential programming). Process communication and synchronization can be achieved either through shared variables (common address space) or by message transmission. It has been shown that the message transmission mechanism leads to a more general computational structure. In this paper we develop the beginnings of a methodology to deal with what we call message oriented programming. We note in passing that the methodology for programming with shared variables is well developed and shows a development leading from operational (automata oriented) constructs (semaphores) to high level programming constructs (critical regions and then monitors). Recent mathematical theories of message oriented programming deal with the subject from an operational point of view. However, the models are too far removed from the control and data structures of programs to guide the designer in constructing a process. To be able to bridge this gap between program specification and program implementation (expressed in the high level language that we use), we resort to a definitional specification technique based on the concept of abstract data type. The specification technique is used in conjunction with some useful design principles to illustrate our ideas via solutions to well-known problems. The two main principles we discuss are: differences (and needs) for definitions of process and message structures in a given application and the concepts of module strength and module coupling as put forward by Myers. Finally, we illustrate how the high level definitional technique leads us to a straightforward method for studying some properties of message oriented programs. We give an example of proving the deadlock freeness of a solution to the consumer and producer problem.