Hoare logic of CSP, and all that

Generalized Hoare logic is a formal logical system for deriving invariance properties of programs. It provides a uniform way to describe a variety of methods for reasoning about concurrent programs, including noninterference, satisfaction, and cooperation proofs. The authors describe a simple meta-rule of the generalized Hoare logic-the decomposition principle-show how all these methods can be derived using it. 19 references.