系统精化关系

先固定精化方向 ​

设规格 $S$ 允许行为集合 $\mathcal{B}(S)$，实现 $I$ 允许行为集合 $\mathcal{B}(I)$。本页采用

$$I⊑S⟺\mathcal{B}(I)\subseteq \mathcal{B}(S),$$

读作“实现精化规格”。实现可以消除规格中的非确定选择、补充内部细节，却不能增加规格禁止的可观察行为。

有些文献把符号方向反过来，因此任何精化定理都应同时写出集合包含或匹配条件。只说“更精”而不说明哪一边允许行为更少，会在传递证明和接口替换中产生方向错误。

若规格性质 $\phi$ 对行为集合按子集封闭，且 $S\models \phi$，则 $I⊑S$ 推出 $I\models \phi$。这与语义蕴涵公理库语义蕴涵Semantic entailment所有满足前提集的结构与赋值也满足结论时成立的语义关系。的结构相同：所有实现行为都落在规格模型允许的范围内。

用模拟证明精化 ​

直接比较无限行为集合通常困难。可建立表示关系 $R$，把每个具体实现状态关联到抽象规格状态，再证明模拟公理库模拟关系Simulation relation · Forward simulation · Weak simulation用方向性的状态关系要求一个系统的每步行为能够由另一个系统匹配。：初始状态被覆盖，每个实现步骤都由规格的一个可见步骤或若干允许的内部步骤匹配。

考虑一个抽象计数器规格，动作 inc 使整数值加一。实现把整数存成二进制位数组，并用多步 carry 传播完成一次 inc。表示函数 $r$ 把位数组解释为整数。

若实现内部 carry 步标作 $\tau$，最终提交步对应抽象 inc，证明责任包括：内部步不改变已提交抽象值；一次完整提交使 $r(c^{\prime })=r(c)+1$；所有合法初始表示映射到规格初态。

仅验证最终几个测试值相等不足以证明精化。还要覆盖溢出、非法位模式、执行中途被观察以及实现非确定调度等边界。

数据精化与操作责任 ​

状态表示改变时，常用 abstraction function $\alpha :C\to A$ 或关系 $R\subseteq C\times A$。每个具体操作 $o{p}_C$ 必须与抽象操作 $o{p}_A$ 交换到允许误差内，可写成

$$R(c,a)\wedge c{\stackrel{op}{\to }}_C{c}^{\prime }⟹\mathrm{\exists }{a}^{\prime },a{\stackrel{op}{\Rightarrow }}_A{a}^{\prime }\wedge R(c^{\prime },a^{\prime }).$$

此外还需 initialization 与 finalization：具体初态对应抽象初态，具体输出经观察函数得到规格允许的结果。忽略输出映射可能让内部状态匹配正确，却向用户返回错误值。

操作前置条件也不能被实现悄悄加强。若规格允许所有非空队列执行 dequeue，实现只能在长度至少二时成功，就减少了调用者受保证的输入范围，通常不构成可替换精化。

添加细节不等于添加行为 ​

实现把一个抽象原子动作细分成多个内部步骤，是添加状态和路径细节；只要这些步骤不可观察且不引入新可见结果，仍可能缩小或保持可见行为集合。

相反，给接口增加一个可见错误返回看似“说明得更详细”，却可能增加规格没有允许的 trace。细节多寡是表示层概念，精化方向由可观察行为包含决定。

消除非确定性通常是合法精化。例如规格允许选择红或蓝，实现固定选择红，行为集合变小。若 liveness 规格依赖最终仍有某选择，过度消除也可能破坏假设；需确认被保存的性质类。

组合与边界 ​

精化若是预序，应满足自反和传递，使多阶段开发可以串联。要在组件上下文中替换实现，还需 congruence：若 $I⊑S$，是否对所有环境 $E$ 都有 $E[I]⊑E[S]$。环境能观察内部时间、故障或资源时，原观察接口可能不够。

trace inclusion 对安全性质很自然，却未必保持所有活性或公平性质。实现可插入无限内部循环，使每个完成的可见 trace 都合法，同时永远不完成规格承诺；divergence-sensitive refinement 要显式排除这种行为。

精化证明也不自动连接到机器代码。若只证明高级模型之间的关系，还需编译器正确性、运行时假设或验证提取链才能把结论传到底层实现。

接口版本演进还要固定观察者能力。旧规格若保证调用 read 不改变状态，新实现增加缓存计数器但计数器不可见，仍可能精化；一旦监控接口暴露该计数器，相同内部步成为可见行为，原证明关系便需重做。这不是兼容层问题，而是行为字母表改变后精化命题本身改变。

精化结论因此总是相对于一份明确的观察契约。

参考资料

• Carroll Morgan, Programming from Specifications, 2nd ed., Prentice Hall, 1994, Chs. 1–5。
• J. M. Spivey, The Z Notation: A Reference Manual, 2nd ed., Prentice Hall, 1992, Chs. 5, 17。
• Nancy A. Lynch and Frits W. Vaandrager, “Forward and Backward Simulations,” Information and Computation 121(2), 1995, pp. 214–233。