We suggest a refinement calculus that satisfies all of the mentioned requirements.
A wide-spectrum language is presented that is general enough to allow the specification of the desired computation in very abstract terms. However, it can also encode a standard language with fair, shared-variable parallelism, synchronization, message-passing and local variables.
A crucial step towards a refinement calculus is the definition of a context-sensitive notion of approximation. It allows the comparison of the behaviour of two programs with respect to a particular environment. The definition requires a slight but crucial change to the semantics by augmenting traces with labels.
A refinement calculus that supports the stepwise development of shared-variable and message-passing parallel programs in a context-sensitive fashion. The rules allow the introduction of local variables, and the proof of certain liveness properties. Most of the rules are compositional.
A variety of detailed examples illustrates the use of the calculus and hopes to show its expressiveness and relative ease of use. One of these examples deals with an n-process mutual exclusion algorithm, contains a derivation from a considerably more high-level representation, and reveals several alternative implementations some of which exhibit more parallelism than the standard textbook version.
Finally, we place our work in context by detailedly discussing related work.