天天看点

软件构造笔记(九)---PPT第五讲行为等价性规约前置/后置条件设计规约

设计规约

  • 行为等价性
  • 规约前置/后置条件
  • 设计规约
    • 规约的强度

行为等价性

举例来说:站在客户的角度,下面两个函数行为是否等价

软件构造笔记(九)---PPT第五讲行为等价性规约前置/后置条件设计规约

分情况:

1.当val缺失时,findFirst返回arr的长度,findLast返回-1

2.当val出现两次时,findFirst返回较低的索引,findLast返回较高的索引。

3.但是当val恰好出现在数组的一个下标处时,这两个方法的行为是相同的。当它们调用这个方法时,它们将传入一个包含一个元素val的arr。对于这样的客户端,这两个方法是相同的。

所以,其实现在没有办法准确定义这两个函数行为是否等价。

但如果我们设计一个spec规约,根据规约判定两个函数是否等价,能看出来,上述两个函数满足改规约,所以函数等价

软件构造笔记(九)---PPT第五讲行为等价性规约前置/后置条件设计规约

如何判断行为等价性:

1.单纯的看实现代码,并不足以判定不同的implmentation是否是“行为等价的”。

2.需要根据代码的spec(开发者与client之间形成的contract)判定行为等价性。

3.在编写代码之前,需要弄清楚spec如何协商形成、如何撰写。

规约前置/后置条件

1.前置条件:对客户端的约束,在使用方法时必须满足的条件

2.后置条件:对开发者的约束,方法结束时必须满足的条件

3.契约:如果前置条件满足了,后置条件必须满足。如果前置条件不满足,则方法可做任何事情。

4.设计特点:

参数由@param子句描述,结果由@return和@throws子句描述。尽可能将前置条件放入@param中,将后置条件放入@return和@throws中。

5.方法的说明可以讨论方法的参数和返回值,但绝不应该讨论方法的局部变量或方法类的私有字段。

6.可变方法的spec:

软件构造笔记(九)---PPT第五讲行为等价性规约前置/后置条件设计规约

前两种都是可变方法,会修改传入的参数,但是除非在后置条件里声明过,否则方法内部不应该改变输入参数。应尽量遵循此规则,尽量不设计mutating 的spec ,否则就容易引发bugs 。

设计规约

规约的强度

1.存在规约S1和S2,判断是否可以用S2替代S1

若满足条件:S2的前置条件更弱、后置条件更强,则证明S2>=S1,可以用S2代替S1

spec变强:更放松的前置条件+更严格的后置条件

越强的规约,意味着implementor的自由度和责任越重,而client的

责任越轻。

2.举例:

(1)前置条件变弱,后置条件不变

判断后置条件是要在满足第一个函数的前置条件的前提下,能发现后置条件相同

软件构造笔记(九)---PPT第五讲行为等价性规约前置/后置条件设计规约

(2)前置条件和后置条件都变弱了,无法判断

软件构造笔记(九)---PPT第五讲行为等价性规约前置/后置条件设计规约