软件构造课程笔记——软件规约

软件规约 Specification

包括软件文档，前置注释等形式

实现者满足规约，使用者依赖规约
规约将实现者和使用者解耦
在遵循规约的前提下，实现者自由变更实现，使用者自由变更用途。

客户视角的等价实现

遵循同一规约的两种可互相替代的实现

方法规约结构

前置条件

方法要求。规约使用者的职责，即方法被调用时的状态。

后置条件

方法效果。规约实现者的职责，即方法被恰当调用后的状态。
方法在前置条件下被调用时，方法必须遵守后置条件。包括返回恰当的值，抛出规定的异常，修改或保持数据对象等。

异常行为

规约的前置条件不被满足时调用方法的行为。

规约设计

确定性规约

对于满足前置条件的一个状态，仅有一种确定的返回值及程序状态。

非确定性规约

对于满足前置条件的一个状态，有多种可能的合法返回值及程序状态。
这意味着规约实现者有多种选择，规约被实现后，行为通常是完全确定的。

操作性规约

给出一系列实现步骤。

宣言性规约

给出最终的输出/状态与初始输入间的关系，不涉及具体实现。

宣言性规约优于操作性规约。当有必要使用操作性注释解释方法的运行原理时，应将操作性注释放置在方法内部，而非方法前的规约部分。

规约强弱性

规约s2 ≥ 规约s1 当且仅当

1. s2 前置条件 ≤ s1 前置条件
2. 对于满足s1前置条件的情况， s2 后置条件 ≥ s1 后置条件

强弱性未必可比

若 s2 ≥ s1
则s2 可以安全地替换 s1

强化规约：削弱前置条件，增强后置条件。