依赖—保证推理

rely 是组件写给环境的“我能承受什么”，guarantee 是组件交给环境的“我最多做什么”。单独验证组件时，不必知道邻居的代码，只需在所有满足 rely 的干扰下维持自己的断言。组装时再核对每份保证是否落在对方依赖内，像把两份接口契约对接起来。

关系摘要比逐个原子语句更稳定。环境可以用完全不同的实现，只要每一步仍在 rely 允许范围内，原证明就可复用。不过摘要不能靠愿望变窄：真实环境若可能减少计数器，而 rely 只允许增加，局部证明的前提在组合系统里并未兑现。

状态含整数 $x$ 和 ghost 位 $a,b\in \{0,1\}$，共享不变式为

线程 A 在 $a=0$ 时唯一一次把 $(x,a)$ 更新为 $(x+1,1)$，保持 $b$；线程 B 在 $b=0$ 时把 $(x,b)$ 更新为 $(x+2,1)$，保持 $a$。记这两个实步关系为 $Astep,Bstep$，令

于是 $G_A\subseteq R_B$、$G_B\subseteq R_A$ 由定义直接成立。A 的实步使 $x$ 与 $a$ 同增一，B 的实步使 $x$ 与 $2b$ 同增二，所以两种关系都保持 $I$。从 $(0,0,0)$ 出发，无论 A、B 哪个先走，两者终止时 $a=b=1$，故 $x=3$。

若另有未建模线程执行 x:=0，它不属于任一 rely，组合结论立即失去前提。把 rely 放宽到任意改写 $x$ 虽然覆盖现实，却会使 $I$ 不再稳定，必须增加协议状态或收紧环境。兼容性仍是安全接口：它不保证某个使能步骤最终发生，也不排除死锁。对细粒度内存，还要说明一次 relation step 对应哪种原子事件。

若 A 的保证误写成“最终令 $a=1$”，它不是一步关系，无法与 B 的 rely 做上述包含检查；环境可能在兑现最终结果前经过 B 无法容忍的中间状态。rely/guarantee 的二态接口约束每个可见干扰步，时序承诺则应另用进展条件表达。

依赖—保证规格支持分层开发：先在抽象共享状态上写关系，再分别精化组件实现。计数器单调性、版本推进、所有权状态机和锁保护协议都能写成二态公式；关系复合还可隐藏组件内部步骤，只向上层暴露稳定保证。

在大型验证中，关系若过于具体会泄露实现，过于宽泛又难以证明有用后置。实践常结合 ghost state、区域或分离资源，使 rely/guarantee 只描述真正共享的抽象状态。无论采用哪种表示，最后都要回到交叉包含与稳定性，而不能用“两个组件遵守同一协议”替代公式检查。