The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. We make use of the rely-guarantee approach to concurrency that facilitates reasoning about interference from concurrent threads in a compositional manner. Recursive programs can be defined as fixed points over a lattice of commands and hence we develop laws for reasoning about fixed points. Loops can be defined in terms of fixed points and hence the laws for recursion can be applied to develop laws for loops. Unlike many approaches to concurrency, we do not assume that expression evaluation is atomic.

翻译：本文旨在提出一组通用、经过机械验证的精化规则，用于在并发环境下推理递归程序与while循环。我们采用依赖-保证方法来处理并发问题，该方法能够以组合方式对来自并发线程的干扰进行推理。递归程序可被定义为命令格上的不动点，因此我们开发了用于推理不动点的法则。循环可借助不动点定义，从而可将递归法则应用于推导循环法则。与许多并发处理方法不同，我们并不假设表达式求值是原子性的。