软件构造 第三章第二节 软件规约

Posted 2020-11-19 masteryellow

第三章第二节 软件spec

 

 

 

客户端无需阅读调用函数的代码，只需理解spec即可。

精确的规约，有助于区分责任，给"供需双方"确定了责任，在调用的时候双方都要遵守。

@param

@return

@throws

 

例子：

 

Behavioral equivalence (行为等价性)

根据规约判断是否行为等价

与实现无关！

 

如果两个函数符合这个规约，故它们等价。

 

 

Specification Structure

前置条件(precondition)：对客户端的约束，在使用方法时必须满足的条件。由关键字 requires 表示；

后置条件(postcondition)：对开发者的约束，方法结束时必须满足的条件。由关键字 effects 表示

异常行为(Exceptional behavior)：如果前置条件被违背，会发生什么

 

确定的规约：给定一个满足前置条件的输入，其输出是唯一的、明确的

欠定的规约：同一个输入可以有多个输出

未确定的规约：同一个输入，多次执行时得到的输出可能不同；但为了避免分歧，我们通常将不是确定的spec统一定义为欠定的规约。

 

操作式规约，例如：伪代码

声明式规约：没有内部实现的描述，只有"初-终"状态，声明式规约更有价值

 

规约强度：

pec变强：更放松的前置条件+更严格的后置条件