Using Hoare Logic in a Process Algebra Setting
Keyword(s):
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.
1985 ◽
Vol 37
◽
pp. 77-121
◽
1985 ◽
Vol 5
◽
pp. 171-199
◽
1997 ◽
Vol 177
(2)
◽
pp. 287-328
◽