规约的强度及其比较

如何写出好的规约

Functions & methods in programming languages

返回值类型是否匹配、参数类型是否匹配，在静态类型检查阶段完成

使用“方法”的客户端，无需了解方法内部（方法体信息隐藏）具体如何工作—“抽象”。

2 Specification: Programming for communication

API：应用程序编程接口

Documenting in programming

“假设”写什么？变量的数据类型定义、final关键字定义了设计决策-“不可改变”、方法假设策略

为什么写？：自己记不住、别人不懂

编程时注意两点目标：代码中蕴含的“设计决策”--给编译器读；注释形式的“设计决策”--给自己和别人读。就是依据假设来进行编程，编程过程需要考虑编译器和读者两部分人。

Specification and Contract (of a method)

Spec给“供需双方”都确定了责任，在调用的时候双方都要遵守：输入输出的数据类型、功能和正确性、性能（只讲能做什么，不讲怎么实现）

Behavioral equivalence 行为等价性

怎么判断是否行为等价性：是否可以用一种实现替代另一种实现（站在客户端视角，前置条件和后置条件）

根据规约判断行为等价性

BehaviorEquivalence

Specification structure: pre-condition and post-condition

方法规约包含几个条文： 1. Precondition 前置条件：对客户端的约束，在使用方法时必须满足的条件（参数），indicated by the keyword requires 2. Postcondition 后置条件：对开发者的约束，方法结束时必须满足的条件（返回值），indicated by the keyword effects 3. Exceptional behavior 异常行为：如果违反先决条件它会做什么。契约--如果前置条件满足了，后置条件必须满足（可以通过抛出异常、修改或不修改对象等来遵循后置条件）；如果前置条件不满足，则方法可以做任何事。

Java 的静态类型声明是一种规约，可据此进行静态类型检查static checking。方法前的注释也是一种规约，但需人工判定其是否满足。前置条件前置条件写进参数 @param，后置条件结果@return, @throws

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

除非在后置条件里声明过，否则方法内部不应该改变输入参数，应尽量不改变输入参数，尽量不设计mutating的spec，应该尽量避免使用mutable的对象，否则就容易引发bugs、降低可变性、复杂化规约。（多个引用指向同一个对象，任意一个引用修改其他的也会引起变化）。

Testing and verifying specifications

依据规约进行黑盒测试（不依赖具体实现，但测试必须遵守契约）。

Designing specifications

Classifying specifications

规约的确定性（输出）、规约的陈述性（输出什么或怎么得到输出）、规约的强度（合法实现的多少）

规约强度越高 (Stronger)，则可以用规约强度高的来代替强度弱的，那么如何比较强度？

更放松的前置条件+更严格的后置条件

越强的规约，意味着implementor的自由度和责任越重，而client的责任越轻（输入内容约束更少）。

下面是两个可以比较、不能比较规约强弱的实例

无法比较 后者更强
StrongerVSWeakerSpecs2

Diagramming specifications 制图规约

某个具体实现，若满足规约，则落在其范围内；否则，在其之外。程序员可以在规约的范围内自由选择实现方式，客户端无需了解具体实现。更强的规约，表达为更小的区域

  • 更强的后置条件意味着实现的自由度更低了->在图中的面积更小
  • 更弱的前置条件意味着实现时要处理更多的可能输入，实现的自由度低了->面积更小
DiagrammingSpecifications

Designing good specifications

  1. 内聚coherent：Spec描述的功能应单一、简单、易理解
  2. strong enough：太弱的spec，client不放心、不敢用 (因为没有给出足够的承诺)。开发者应尽可能考虑各种特殊情况，在post-condition给出处理措施。
  3. weak enough：太强的spec，在很多特殊情况下难以达到，给开发者增加了实现的难度。
  4. use abstract types：在规约里使用抽象类型，可以给方法的实现体与客户端更大的自由度。在Java中这意味着使用接口类型，像 Map、Reader 而不是具体实现类型像 HashMap、FileReader。
  5. Precondition or postcondition：是否使用前置条件取决于(1) check的代价；(2) 方法的使用范围。如果只在类的内部使用该方法(private)，那么可以不使用前置条件，在使用该方法的各个位置进行check——责任交给内部client；如果在其他地方使用该方法(public)，那么必须要使用前置条件，若client端不满足则方法抛出异常。