The above list of requirements for our calculus is fairly large. Some of them are in tension with each other and a right balance needs to be found.
Compositionality, for instance, is hard to achieve in the presence of concurrency and liveness properties. Assumption-commitment reasoning as proposed by Jones yields a compositional treatment of concurrency which we will make use of. Moreover, liveness property are often very difficult to prove because the proof requires a global view of the entire system. Since liveness properties are vital, the challenge is to make their proofs as modular and thus as tractable as possible. Finally, fairness also needs to be modeled compositionally. Most treatments of fairness are operational [Fra86,AO83] and a denotational approach is still perceived to be difficult. However, based on early work by Park [Par79], Brookes and Older have shown that this perception is unjustified [Bro96b,Old96].
A suitable wide-spectrum language needs to bridge the two extreme ends of a spectrum. On the one hand, desired properties have to be expressed in a high-level, abstract fashion. On the other hand, the low-level, detailed view of an executable program needs to be supported. Moreover, both safety and liveness properties need to be expressible.
We face a similar situation when determining the rules of the calculus. A large number of rules guarantees applicability of the methodology in a large variety of settings, but may also lead to confusion.
Moreover, the wealth of paradigms and mechanisms in parallel programming has given rise to an even more confusing wealth of different models for these paradigms. For instance, shared-variable concurrency has been modeled using a variety of state traces and temporal logics. Message-passing concurrency on the other hand has been modeled using, for instance, synchronization trees (CCS, [Mil89]), or failure-divergence traces (CSP, [BHR84]). The refinement of a shared-variable program into a distributed, message-passing program, however, requires a uniform semantic model.
Finally, the introduction of parallelism, synchronization and communication are crucial points in the development. It is not clear how a calculus can best support them.