用依赖/保证逻辑补充命令式进程代数
Complementing an imperative process algebra with a rely/guarantee logic
AI总结：
本文为命令式进程代数ACP的扩展补充了依赖/保证逻辑，用于推理进程执行中数据变化，并证明其在处理相互干扰的并行进程时比Hoare逻辑更合适。
摘要：
本文关注命令式进程代数与依赖/保证逻辑之间的关系。一个命令式进程代数由一个依赖/保证逻辑加以补充，该逻辑可用于推理数据在进程执行过程中如何变化。所使用的命令式进程代数是ACP（通信进程代数）的扩展，该扩展此前已在一篇关于命令式进程代数与Hoare逻辑关系的论文中使用过。一个涉及部分正确性判断的补充性依赖/保证逻辑被详细处理。该逻辑对弱完全正确性和强完全正确性的适配也被讨论。文中给出一个简单示例，表明在涉及相互干扰的并行进程时，依赖/保证逻辑比Hoare逻辑更适合作为补充逻辑。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
