在做了三次实验后，对怎么写一个好的规约，做点个人的总结。

规约，在静态类型检查阶段检查参数类型是否匹配，返回值类型是否匹配也在静态检查阶段完成。 静态类型声明是一种规约，可据此进行 静态类型检查static checking 方法前的注释也是一种规约，但需人工判定其是否满足。 一个完整的方法包括了方法的规约和方法的实现体。 行为等价性：站在客户端的视角看行为等价性，根据规约判断函数的行为等价性，前置条件相同时，返回结果一样就等价。要根据代码的规约来判断行为等价性。

前置条件：对客户端的约束，在使用方法时必须满足的条件。 后置条件：对开发者的约束，方法结束时必须满足的条件。 如果前置条件满足了，后置条件必须满足。（前置条件不满足，则方法可以做如何事情。） 前置条件位于@pram后，而后置条件位于@return与@throws后。

规约不应该讨论方法的局部变量或方法类的私有字段。规约不声明变量类型。

太弱的spec，client不放心、不敢用 (因为没有给出足够的承诺)。 开发者应尽可能考虑各种特殊情况，在post-condition给出处理措施。 太强的spec，在很多特殊情况下难以达到，给开发者增加了实现的难度（client当然非常高兴）。

不写Precondition，就要在代码内部check；若代价太大，在规约里加入precondition， 把责任交给client。 客户端不喜欢太强的 precondition，不满足precondition的输入会导致失败。惯用做法是：不限定太强的precondition，而是在postcondition中抛出异常：输入不合法，尽可能在错误的根源处fail，避免其大规模扩散。

归纳：是否使用前置条件取决于(1)check的代价；(2)方法的使用范围 – 如果只在类的内部使用该方法(private)，那么可以不使用前置条件，在使用该方法的各个位置进行check——责任交给内部client； – 如果在其他地方使用该方法(public)，那么必须要使用前置条件，若client端不满足则方法抛出异常。