第三章第二节 软件spec
客户端无需阅读调用函数的代码，只需理解spec即可。
精确的规约，有助于区分责任，给"供需双方"确定了责任，在调用的时候双方都要遵守。
@param
@return
@throws
例子：
Behavioral equivalence (行为等价性)
根据规约判断是否行为等价
与实现无关！
如果两个函数符合这个规约，故它们等价。
Specification Structure
前置条件(precondition)：对客户端的约束，在使用方法时必须满足的条件。由关键字 requires 表示；
后置条件(postcondition)：对开发者的约束，方法结束时必须满足的条件。由关键字 effects 表示
异常行为(Exceptional behavior)：如果前置条件被违背，会发生什么
确定的规约：给定一个满足前置条件的输入，其输出是唯一的、明确的
欠定的规约：同一个输入可以有多个输出
未确定的规约：同一个输入，多次执行时得到的输出可能不同；但为了避免分歧，我们通常将不是确定的spec统一定义为欠定的规约。
操作式规约，例如：伪代码
声明式规约：没有内部实现的描述，只有"初-终"状态，声明式规约更有价值
规约强度：
pec变强：更放松的前置条件+更严格的后置条件
