规格 | Codeboy's Blog

形式陈述

规格规定哪些结果或行为被允许。对输入集合 $I$ 与输出集合 $O$ ，它可以是关系

S\subseteq I\times O.

实现 $f:I\to O$ 满足该规格，当且仅当

\forall i\in\operatorname{Dom}(S),\quad(i,f(i))\in S.

这里的全称量词只覆盖规格定义域；若预期输入被漏出 $\operatorname{Dom}(S)$ ，验证不会替需求补上它。关系也不必给每个输入唯一输出，多种结果可以同时正确。

有状态系统需要比较完整行为。令 $Obs$ 把实现执行投影到规格可见的行为域 $B$ ，并定义

Beh_{Obs}(M)=\{Obs(\rho):\rho\text{ 是 }M\text{ 的允许执行}\}.

若 $B_S\subseteq B$ 是规格允许的行为集合，则满足关系的统一形式是

M\models_{Obs}S \quad\Longleftrightarrow\quad Beh_{Obs}(M)\subseteq B_S.

程序逻辑的前置/后置条件、状态机不变量、时序逻辑公式与并发对象的调用—返回历史，都是选择不同 $B$ 与 $Obs$ 后的规格。安全性质通过有限坏前缀排除行为，活性性质则约束完整无限执行。

$M\models S$ 只有在行为域、观察函数和量词范围固定后才有意义。必须说明收集全部路径还是最大路径、是否保留有限终止执行，以及公平性是否限制无限路径；这些不是记号自动携带的约定。

环境假设 $A$ 与系统保证 $G$ 可写成

Beh_{Obs}(M)\cap A\subseteq G.

该式只约束满足 $A$ 的行为。若 $A=\varnothing$ 或 $A\cap Beh_{Obs}(M)=\varnothing$ ，保证会真空成立，所以还要独立检查假设可满足且确实覆盖预期环境。

直觉

规格回答“哪些行为算正确”，实现回答“系统实际怎样产生行为”。证明逐一说明实现行为经观察后落入允许集合；反例搜索则尝试构造

Beh_{Obs}(M)\cap(B\setminus B_S)

中的元素。测试只采样这个差集，模型检查或演绎证明才试图覆盖规定量词域中的全部行为；精化则比较两个允许集合谁更具体。

形式化不会保证需求本身正确。规格可能遗漏输入、允许过多行为、把环境责任错写给系统，甚至彼此矛盾。验证结论始终是“相对于这个规格正确”，不能替代需求评审。

例子与边界

排序规格可要求输出 $y$ 与输入 $x$ 含有相同多重集合且非降排列；它不规定 quicksort、mergesort、稳定性或内部比较轨迹。这说明规格既可约束结果，又可有意隐藏实现策略。

整数平方根给出更小的手算例。对 $n\in\mathbb N$ ，允许输出 $r\in\mathbb N$ 当且仅当

r^2\le n<(r+1)^2.

输入 $n=10$ 时， $r=3$ 满足 $9\le10<16$ ； $r=2$ 因 $10<9$ 为假而失败， $r=4$ 因 $16\le10$ 为假而失败。这个检查只使用输入—输出关系，不要求实现采用二分搜索还是逐次试探。

并发队列通常量化调用—返回历史，分布式复制协议还可能量化消息、故障与无限执行。若把两者都压成最终状态关系，实时顺序与进展责任会消失；最终数据相同不能证明中途返回值或可用性正确。

“程序没有崩溃”只是很弱的安全性质，不等于功能正确；“每个请求最终响应”是活性条件，也不保证响应内容正确。成本上界、概率错误与近似比只有被写入规格或单独保证时，才属于待验证合同。

若规格只量化无限公平执行，一个停在未响应请求上的有限最大执行可能被排除；对持续服务而言，这会掩盖死锁。应先说明哪些有限执行算完整行为，再说明哪些无限调度因公平假设被接受，而不是让“活性”一词代替这些选择。

推论与应用

算法正确性把实现执行与规格比较；精化把较具体行为限制到较抽象规格允许的范围；模型检查判定有限状态模型是否满足给定性质。

规格设计常先固定观察接口，再区分环境假设与系统保证。模块化验证依赖此边界：调用方只需依赖公开规格，被调用模块可以替换实现，只要继续满足同一合同。

参考资料

Leslie Lamport, Specifying Systems, Addison-Wesley, 2002, Chapters 1–3.
Carroll Morgan, Programming from Specifications, 2nd ed., Prentice Hall, 1994, Chapters 1–2.
Michael Huth and Mark Ryan, Logic in Computer Science, 2nd ed., Cambridge University Press, 2004, Chapters 2–3.
Bowen Alpern and Fred B. Schneider, “Defining Liveness,” Information Processing Letters 21(4), 1985, pp. 181–185.