系统精化关系

数据精化与操作责任 ​

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

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

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

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

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

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

消除非确定性通常是合法精化。例如规格允许选择红或蓝，实现固定选择红，行为集合变小。对“每条完整执行最终返回结果”这类全称轨迹性质，只要行为集合确实包含无限执行并保持包含关系，删除选择仍会保持性质。对“仍存在一条选择蓝色的路径”则不同：它要求保留某个可能性，单纯行为包含并不保证它。

组合与边界 ​

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

只比较有限可见 trace 时，活性或公平性可能丢失。实现可插入无限内部循环，使每个有限可见前缀都合法，却永远不完成规格承诺。若比较对象已经包含完整无限行为，并且性质是逐行为的全称条件，集合包含本身仍保持该性质；失效来自有限观察隐藏了发散，或公平路径的定义没有随精化正确对应。发散敏感的精化要显式处理这一证明义务。

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

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

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