  This paper concerns the relation between process algebra and Hoare logic. We
investigate the question whether and how a Hoare logic can be used for
reasoning about how data change in the course of a process when reasoning
equationally about that process. We introduce an extension of ACP (Algebra of
Communicating Processes) with features that are relevant to processes in which
data are involved, present a Hoare logic for the processes considered in this
process algebra, and discuss the use of this Hoare logic as a complement to
pure equational reasoning with the equational axioms of the process algebra.

Logic in Computer Science