目标

规约，前置后置条件，欠定规约、非确定规约、陈述式、操作式规约、规约的强度及其比较

规约

作用

1. 给自己和别人写出设计决策：如final、数据类型定义
2. 作为契约，服务端与客户端达成一致
3. 调用方法时双方都要遵守
4. 便于定位错误
5. 解耦，无需告诉客户端具体实现，变化也无需通知客户端，扮演防火墙角色
6. 判断行为等价性

内容

1. 输入输出的数据类型
2. 功能和正确性
3. 性能

行为等价性

站在客户端视角看一个行为是否具有等价性。如果两个函数都符合同一个Spec，则他们等价

Spec的结构

1. 前置条件：对客户端的约束，在使用方法时必须满足的条件，用@param，并用@requires进行说明
2. 后置条件：对开发者的约束，方法结束时必须满足的条件，用@return和@throws，并用@effects进行描述
3. 契约：前置条件满足了，则后置条件必须满足
   Spec不需要说明方法内部变量和类的私有方法或变量
   
   标签：规约,方法,Specification,cache,HITSC,Designing,static,前置条件,客户端
   From： https://www.cnblogs.com/Ch1ldKing/p/18216410