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. © 1984, ACM. All rights reserved.