# Using Hoare logic in a process algebra setting

## TL;DR

This paper explores integrating Hoare logic with process algebra, specifically extending ACP to reason about data changes within processes and complement equational reasoning.

## Contribution

It introduces an extension of ACP with data features and develops a Hoare logic tailored for reasoning about data modifications in process algebra.

## Key findings

- Extended ACP with data features
- Developed a Hoare logic for data reasoning
- Complemented equational reasoning with Hoare logic

## Abstract

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.