目录
1 方法的“行为等价性”
2 规约spec的结构
3 规约spec的形式
4 比较spec
4.1 确定性
4.2 陈述性
4.3 强度
5 spec的图形化
6 关于“是否使用precondition”的问题
1 方法的“行为等价性”
首要：站在客户端的角度。
因此无论代码内部如何相似，如何差距之大，都需要通过spec来判断“行为等价性”。
上述两个方法在开发者看来最后的结果并不一定一样。
但是在客户端看来，若结合spec：
这两个方法都符合这个规约，因此在客户端眼里，这两个方法是等价的。
2 规约spec的结构
前置条件precondition：对客户端client的约束，尽可能地在requires中体现；
后置条件postcondition：对开发者implementers的约束，尽可能地在effects中体现；
契约：若满足precondition，则必须满足postcondition。
同样的，若不满足precondition，则方法可以做任何事。（但是开发者应该有“道德”去throw异常，以fail fast）
3 规约spec的形式
参数：@param，尽量描述precondition；
结果：@return和@throws，尽量描述postcondition。
4 比较spec
标准：确定性、陈述性、强度
4.1 确定性
确定的规约deterministic：对满足precondition的输入，只有唯一的输出。
欠定的规约underdeterministic：对满足precondition的输入，有多个输出，且通常有确定的实现。
非确定的规约nondeterministic：对同一个输入，多次执行得到的结果不同。
4.2 陈述性
操作式规约operational：给出一系列执行方法的细节，例如：伪代码。
陈述式规约declarative：无内部实现的描述，只有“初-终”状态；陈述式规约更有价值。
4.3 强度
若规约强度S2>=S1，则可以用S2替换S1。
当precondition越弱，postcondition越强，spec的强度越高。
注意：比较postcondition的强度要在相同的precondition下：
在上述例子中，后者比前者前置条件变弱，后置条件强度不变，因此后者总体强度在前者之上。
注意：存在两个方法无法比较强度。
只要是在加强spec，就可以修改规约，而不需要重新考虑其他的实现。
5 spec的图形化
每个点代表一个方法；
规约spec划定一个范围：若method满足规约，则此method代表点就落在范围内；
强spec表达为更小的区域。
6 关于“是否使用precondition”的问题
取决于check的代价和方法的使用范围。
check是指在postcondition中抛出异常，而给予client极大的自由度，即上述“体现开发者道德之处”，但是若check代价过大，则要限制client的自由。
在类内部使用的方法（private），可以不使用precondition；
在其他使用的方法（public），必须使用precondition。
文章知识点与官方知识档案匹配，可进一步学习相关知识Java技能树首页概览91508 人正在系统学习中
声明：本站部分文章及图片源自用户投稿，如本站任何资料有侵权请您尽早请联系jinwei@zod.com.cn进行处理,非常感谢！