精化演算

命令作为谓词变换器 ​

把命令 $S$ 解释为弱前置变换器公理库最弱前置条件Weakest precondition保证程序建立给定后置条件的最弱状态谓词。 $wp(S,Q)$。若对所有后置条件 $Q$ 都有

$$wp(S,Q)\Rightarrow wp(T,Q),$$

则在本页约定下，$T$ 是 $S$ 的实现精化，记作

$$S⊑T.$$

含义是：任何足以保证规格命令 $S$ 达到 $Q$ 的初态，也足以保证更具体命令 $T$ 达到 $Q$。文献可能反写符号，必须结合蕴含式确认方向。

这与行为精化公理库系统精化关系Refinement relation · System refinement · Specification refinement以行为包含、模拟或表示映射约束实现，使其允许行为不超出规格。相接，但谓词变换器还编码终止是 partial 还是 total correctness；选择 $wp$ 或 weakest liberal precondition 会改变次序。

健康谓词变换器通常还要求 strictness、conjunctivity 等性质。demonic command 对任意后置集取逆像并要求所有可能结果满足，因此保存任意 meet；angelic nondeterminism 则更接近保存 join。选择哪些健康条件决定该演算对应哪类程序语义。

abort、magic 与 skip 是边界命令：abort 无法保证后置，magic 无需执行即可满足任意后置，skip 保持状态。混淆 abort 和 magic 会让不可实现规格看似最强实现。

规格语句 ​

规格语句 $[P,Q]$ 表示从满足 $P$ 的初态出发，终止于满足关系后置 $Q(s,s^{\prime })$ 的某状态。它允许所有符合契约的实现，而未规定计算步骤。

例如“输入 $n\ge 0$，输出 $r$ 满足 $r^2\le n<(r+1{)}^2$”先写成规格，再逐步选择二分或线性搜索。两种算法都可精化同一契约，性能不是基础精化关系自动比较的对象。

若后置关系无可实现状态，规格 miraculous；若前置为 false，任何实现都 vacuously 满足。演算需排除或显式处理这些退化规格，不能把逻辑蕴含通过当成可部署程序。

feasibility 条件要求允许初态至少有一个后继满足关系。对 total correctness，规格还要求实现终止；把非终止作为“没有坏后继”会错误满足任意后置。

非确定规格可以有多个合法结果。实现选择其中一个通常是 refinement；若环境而非实现控制选择，消除某些分支可能违反输入接受义务。接口需区分输入 nondeterminism 与内部实现 freedom。

赋值精化轨迹 ​

目标规格为从 $x\ge 0$ 产生 $y=x+1$。选择赋值 y:=x+1，其

$$wp(y:=x+1,Q)=Q[y\leftarrow x+1].$$

代入后置 $Q\equiv y=x+1$ 得 true，因此前置 $x\ge 0$ 蕴含它，赋值满足规格。

若选 y:=x，代入得到 $x=x+1$，在允许初态上为假，精化义务失败。这个失败与具体测试值无关，是整个前置区域的逻辑反例。

对数组更新 A[i]:=v，后置替换不是文本替换所有 $A[j]$，而是 $store(A,i,v)$，读取用 $select$ 并按 $i=j$ 分支。忽略别名索引会证明错误的元素保持性质。

并行赋值 x,y:=y,x 同时读取旧值；若按两个顺序赋值精化，会得到两个变量都等于旧 $y$。选择实现语句必须保持原子赋值语义。

顺序、选择与循环规则 ​

顺序组合满足

$$wp(S;T,Q)=wp(S,wp(T,Q)).$$

非确定 demonic choice 要对所有选择保证后置，因此 wp 取合取；angelic choice 只需存在成功选择，取析取。把两者混用会把实现控制权与环境控制权倒置。

循环精化需要 invariant $Inv$、guard 和 variant。invariant 证明初始化与保持，退出推出后置；variant 落在良基集并严格下降，证明 total correctness 的终止。

只给出一个看起来递减的整数不够，还需证明循环期间非负且每次执行确实严格下降。

guarded command if G_i -> S_i fi 的 demonic 语义要求所有为真 guard 分支都满足后置，并要求至少一个 guard 为真以避免 abort。把 guard 合取成互斥不是演算自动性质；重叠 guard 正是 nondeterminism 来源。

循环 invariant 可先从规格中推导而不是猜测：计算希望保持的抽象关系，再选择实现体。若 invariant 太弱，退出推不出后置；若太强，初始化失败。

单调性与逐步推导 ​

健康谓词变换器通常对后置条件单调：$Q\Rightarrow R$ 推出 $wp(S,Q)\Rightarrow wp(S,R)$。这保证 strengthening/weakening 规则方向一致。

精化的传递性允许链

$$Spec⊑S_1⊑\cdots ⊑Program.$$

每步只承担局部证明义务，最终由传递性得到程序满足初始规格。若中间步骤改变状态空间或数据表示，还需 coupling invariant/refinement mapping。

数据精化例：抽象集合用无序数学 set 表示，实现用无重复排序数组。coupling invariant 连接数组元素集合与抽象 set；insert 操作需证明数组更新后仍有序无重复，且抽象投影恰好多一个元素。

若实现保留 tombstone 或额外容量，它们是具体状态细节；finalization/observation 映射必须隐藏它们。只证明元素数相同不能推出成员集合相同。

边界 ​

演算证明功能正确性，不自动给时间、空间、数值稳定性或并发公平保证；这些需加入规格或独立分析。

从数学关系推导代码还要连接语言溢出、异常和 I/O。精确整数演算得出的赋值在固定宽度机器上可能不保持同一后置。

性能 refinement 需要另加 cost semantics。功能行为集合缩小的实现可能从常数时间变成指数时间，仍满足基础精化关系；实时系统若把 deadline 当保证，就必须把时间纳入观察。

机械演算可以生成大量 verification conditions，最终仍需求解器或证明助理检查。未解决义务不能以“设计直觉清楚”视为已精化。

参考资料

• Ralph-Johan Back and Joakim von Wright, Refinement Calculus: A Systematic Introduction, Springer, 1998, Chs. 1–8。
• Carroll Morgan, Programming from Specifications, 2nd ed., Prentice Hall, 1994, Chs. 1–9。
• Edsger W. Dijkstra, A Discipline of Programming, Prentice Hall, 1976, Chs. 1–4。