A communication data type for message oriented programming

In this report we resort to a definitional specification technique in order to be able to bridge the gap between program specification and program implementation (expressed in a high level application language) in message oriented programming. We show how the notion of algebraic specification can be used to formalize the communications primitives and then applied to the verification of communications properties of parallel programs. We illustrate the method by introducing elements of a calculus for reasoning about message passing programs and then using a specification of the consumer and producer problem and showing that the proposed solution is deadlock free.