Abstract
This paper concerns the relation between imperative process algebra and
rely/guarantee logic.
An imperative process algebra is complemented by a rely/guarantee logic
that can be used to reason about how data change in the course of a
process.
The imperative process algebra used is the extension of ACP (Algebra of
Communicating Processes) that is used earlier in a paper about the
relation between imperative process algebra and Hoare logic.
A complementing rely/guarantee logic that concerns judgments of partial
correctness is treated in detail.
The adaptation of this logic to weak and strong total correctness is
also addressed.
A simple example is given that suggests that a rely/guarantee logic is
more suitable as a complementing logic than a Hoare logic if interfering
parallel processes are involved.