目录
编程中的方法和函数
方法签名
规约：沟通
行为等价性
规约的结构：前置条件和后置条件
可变类型的规约
利用规约进行测试
设计规约
图形化规约
设计好的规约
内聚性
信息丰富
强（功能足够明确）
弱（要能够实现）
使用抽象类型
Precondition?
编程中的方法和函数
方法签名
就是对方法的定义，作用域，返回类型，名称，参数
规约：沟通
减少错误，方便开发，有助于区分责任。能够隔离“变化”，无需通知客户端
只要规约不变，我就不关注方法内部如何实现。所以规约是客户端和开发者之间的桥梁。开发者按照规约进行编程，设计出满足规约的方法，然后客户端依照规约的要求使用即可。
行为等价性
站在客户端角度来看行为是否等价，根据规约判断，只要满足规约就是等价的。
规约的结构：前置条件和后置条件
前置条件：requires，是对客户端的约束，在使用时必须满足的条件
后置条件：effects，是对开发者的约束，方法结束时必须满足的条件，有时包括对异常的处理。
当前置条件满足时，后置条件必须满足。但前置条件不满足，那么方法就可以做任何事情，但最好抛出异常，这样能通过快速失败使bug更容易被找到和修复。除非在后置条件中特殊声明，否则方法不应该改变输入参数
一个规约实现的错误例子
可变类型的规约
后置条件中明确说明要求客户端不更改返回值（靠客户端的良心）或者返回一个可变对象的副本（靠开发者的良心），都不靠谱
最好还是要尽可能使用不可变数据类型
利用规约进行测试
根据一开始设计好的规约，设计黑盒测试用例
设计规约
规约的几个标准：确定性（描述输出是否确定）、陈述性（不对如何实现进行说明）、强度（前置条件更弱或相等，后置条件更强或相等。更少的要求，更多的承诺。很少的实现，更多的用户）规约的强度的比较例子如下：
在进行判断后置条件谁强谁弱时，就根据强的前置条件下，两个规约的后置条件的强度。
如果两个条件矛盾，那么就无法比较
图形化规约
用椭圆内的区域表示所有对规约的实现，椭圆内的每个点表示一种实现。椭圆的面积表示规约的实现有多少种。程序员可以在规约范围内自由选择实现方式，客户端也无需了解具体使用了哪个实现。
更强的规约表达为更小的区域。
更强的后置条件-->实现的自由度更低-->在图中的面积更小
更弱的前置条件-->要处理更多的可能输入-->实现的自由度更低-->面积更小
设计好的规约
内聚性
Spec描述的功能应单一，简单，易理解。所以要把做了两件事的规约分开形成两个方法。
信息丰富
不会让客户端产生理解的歧义。
强（功能足够明确）
要给出足够的承诺
弱（要能够实现）
在这个例子中，如果文件不存在或者是读还是写都不确定，难以进行保证
使用抽象类型
在规约里使用抽象类型，可以给方法的实现体与客户端更大的自由度
Precondition?
如果不写precondition，就要在内部进行check；如果这样做的代价太大，那就在规约里加入precondition，把责任交给客户
惯用做法：不限定太强的precondition，而是在postcondition中抛出异常：输入不合法。
理念：尽可能在错误的根源处fail，避免其大规模扩散。
归纳：是否使用前置条件取决于check的代价和方法的使用范围。只在类的内部使用该方法（private），那么可以使用前置条件（方法内部不需要判断输入是否满足，认为client会保证前置条件），在使用该方法的各个位置进行check，责任交给client；如果在其他地方使用该方法（public），那么可以放松/不使用前置条件（在方法内部检查是否满足），若client不满足方法则抛出异常。
