While our research builds on a very large body of existing work, it mainly draws from the following three sources. A more detailed discussion of related work can be found in Section 9.
The choice of the underlying semantics requires a close look at models for concurrent programming. We have chosen Brookes transition trace semantics which in turn was influenced by Park's work on modeling fairness [Bro96b,Par79].
Research on compositional proof systems for concurrent programs has successfully reconciled concurrency and compositionality using assumption-commitment reasoning [Jon81]. We use a form of assumption-commitment reasoning that is due to Stirling [Sti88].
Finally, a number of refinement calculi for sequential programs have been proposed [Mor87,Mor89,Heh93]. This work provided intuition and clarified some general questions about program design through stepwise refinement.