The "Hoare Logic" of CSP, and All That

Abstract

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. We describe a simple meta-rule of the Generalized Hoare-Logic - the Decomposition Principle - and show how all these methods can be derived using it.