Specification
linchpin of teamwork 明确双方的责任 客户端无需看懂调用函数的代码，只需理解spec即可
规约结构
1.前置条件 requires
对客户端的约束，使用方式必须满足的条件
2.后置条件 effects
对开发者的约束，方法结束时必须满足的条件 前置条件满足，后置条件必须满足 ----契约 前置条件不满足，则方法可以做任何事情
java中的规约
static类型声明是一种规约，可以据此进行静态检查 注释也是一种规约，但需要人工判断 前置条件 ： @param 参数 不需要写类型 后置条件 : @return @throws 方法最好不要改变参数
设计规约
比较两个规约 *
S2 ≥ S1 ： S2的前置条件更弱（可相同），后置条件更强（可相同） S2可替换S1 越强的规约意味着开发者的自由度和责任越重，而使用者的责任越轻
欠定的规约
同一个输入可能有多个输出 同一个输入，多此执行结果可能不同（随机数或timing）
操作式VS声明式
操作式：伪代码 声名式：只有“处->终”状态 √ 应选择对客户端和维护者最清晰的规约
设计规约
不限定太强的precondition 而是在post condition中抛出异常，输入不合法
