在依赖/保证并发中处理局部化：一种代数方法
计算机科学中的逻辑
2019-07-10 v1
摘要
Jones 的依赖/保证方法通过引入依赖(rely)和保证(guarantee)条件扩展了 Hoare 逻辑，以支持对共享变量并发程序的组合式推理。本文关注依赖/保证并发语境下的局部化问题，以支持局部变量。由于我们允许局部变量块的主体包含并行运行的组件进程，该方法需要允许块内局部的变量成为其并行组件进程间的共享变量。为支持依赖/保证方法的机械化，我们开发了一种同步并发精化代数。其基础由一组少量基本命令和少量基本算子构成，其余所有构造均由它们定义。为支持局部变量，我们向代数中添加一个基本局部化算子，用于定义局部变量块。由此可证明局部化的性质，包括其与依赖和保证条件的交互。
引用
@article{arxiv.1907.04005,
title = {Handling localisation in rely/guarantee concurrency: An algebraic approach},
author = {Larissa A. Meinicke and Ian J. Hayes},
journal= {arXiv preprint arXiv:1907.04005},
year = {2019}
}
备注
16 pages