Complementing an imperative process algebra with a rely/guarantee logic

TL;DR

This paper integrates rely/guarantee logic with an extended imperative process algebra based on ACP to enhance reasoning about data changes and correctness in concurrent processes, especially with interference.

Contribution

It introduces a rely/guarantee logic tailored for an extended ACP process algebra, addressing partial and total correctness in concurrent process reasoning.

Findings

Rely/guarantee logic complements imperative process algebra effectively.

The logic handles partial and total correctness in concurrent processes.

Example suggests better suitability of rely/guarantee logic over Hoare logic for interfering processes.

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.