2025/02/05 by C.A. Middelburg, Middelburg, C. A.
Computer Science · #Cognitive Computing and Networks #D.1.3 #D.2.4 #F.1.2 #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.2502.03320
openalex publication_date 2025/02/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.