规约的强度及其比较
如何写出好的规约
Functions & methods in programming languages
返回值类型是否匹配、参数类型是否匹配,在静态类型检查阶段完成
使用“方法”的客户端,无需了解方法内部(方法体信息隐藏)具体如何工作—“抽象”。
2 Specification: Programming for communication
API:应用程序编程接口
Documenting in programming
“假设”写什么?变量的数据类型定义、final关键字定义了设计决策-“不可改变”、方法假设策略
为什么写?:自己记不住、别人不懂
编程时注意两点目标:代码中蕴含的“设计决策”--给编译器读;注释形式的“设计决策”--给自己和别人读。就是依据假设来进行编程,编程过程需要考虑编译器和读者两部分人。
Specification and Contract (of a method)
Spec给“供需双方”都确定了责任,在调用的时候双方都要遵守:输入输出的数据类型、功能和正确性、性能(只讲能做什么,不讲怎么实现)
Behavioral equivalence 行为等价性
怎么判断是否行为等价性:是否可以用一种实现替代另一种实现(站在客户端视角,前置条件和后置条件)
根据规约判断行为等价性
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的责任越轻(输入内容约束更少)。
下面是两个可以比较、不能比较规约强弱的实例
无法比较 | 后者更强 |
---|---|
Diagramming specifications 制图规约
某个具体实现,若满足规约,则落在其范围内;否则,在其之外。程序员可以在规约的范围内自由选择实现方式,客户端无需了解具体实现。更强的规约,表达为更小的区域
- 更强的后置条件意味着实现的自由度更低了->在图中的面积更小
- 更弱的前置条件意味着实现时要处理更多的可能输入,实现的自由度低了->面积更小
Designing good specifications
- 内聚coherent:Spec描述的功能应单一、简单、易理解
- strong enough:太弱的spec,client不放心、不敢用 (因为没有给出足够的承诺)。开发者应尽可能考虑各种特殊情况,在post-condition给出处理措施。
- weak enough:太强的spec,在很多特殊情况下难以达到,给开发者增加了实现的难度。
- use abstract types:在规约里使用抽象类型,可以给方法的实现体与客户端更大的自由度。在Java中这意味着使用接口类型,像 Map、Reader 而不是具体实现类型像 HashMap、FileReader。
- Precondition or postcondition:是否使用前置条件取决于(1) check的代价;(2) 方法的使用范围。如果只在类的内部使用该方法(private),那么可以不使用前置条件,在使用该方法的各个位置进行check——责任交给内部client;如果在其他地方使用该方法(public),那么必须要使用前置条件,若client端不满足则方法抛出异常。