规格

形式陈述 ​

规格是对系统允许行为的数学描述。对输入—输出任务，可写成关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。

$$S\subseteq I\times O,$$

其中实现 $A:I\to O$ 满足规格，当且仅当

$$\mathrm{\forall }i\in \mathrm{Dom}(S),(i,A(i))\in S.$$

规格不必为每个输入指定唯一输出；它可以允许多个正确结果。

对有状态系统，规格可描述初始状态集合、一步转移关系与可观察轨迹集合。安全性质排除有限坏前缀，活性性质要求某类好事件最终发生。程序逻辑中的前置/后置条件、状态机不变量、时序逻辑公式与顺序对象的操作历史规范，都是不同观察层次上的规格。

实现 $M$ 满足规格 $S$ 通常记作

$$M\models S.$$

该符号的含义必须同时给出行为域、观察函数和量词范围；否则“满足”没有固定内容。

直觉 ​

规格回答“哪些行为算正确”，实现回答“系统实际怎样产生行为”。两者分开后，证明可以检查实现是否落在允许集合内，测试可以寻找违反条件的实例，精化可以比较一个描述是否比另一个更具体。

规格不是自然语言愿望的自动翻译。它本身也可能遗漏需求、允许过多行为或相互矛盾；形式验证保证的是相对于给定规格的正确性。

例子与边界 ​

排序规格可以允许任意输出序列 $y$，只要求 $y$ 与输入 $x$ 含有相同多重集合且非降排列。它不规定 quicksort、mergesort 或稳定排序，也不要求唯一的内部比较轨迹。

并发队列的规格通常量化调用—返回历史；分布式复制协议则可能量化消息、故障与无限执行。若把两者都压成最终状态关系，会丢掉实时顺序或进展条件。

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

推论与应用 ​

算法正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。把实现执行与规格比较；精化公理库系统精化关系Refinement relation · System refinement · Specification refinement以行为包含、模拟或表示映射约束实现，使其允许行为不超出规格。把较具体行为限制到较抽象规格允许的范围；模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。判定有限状态模型是否满足给定性质。

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

参考资料

• 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.