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