软件构造复习小结（2）——设计规约（Specification）

软件构造复习小结（2）——设计规约（Specification）

一、方法（Method）

“方法”是程序的“积木”，可以被独立开发、测试、复用；使用“方法”的客户端，无需了解方法内部具体如何工作— “抽象”。

二、行为等价性（Behavioral equivalence）

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

这两个函数满足这个规约即等价。

单纯的看实现代码，并不足以判定不同的implementation是否是“行为等价的”需要根据代码的spec（开发者与client之间形成的contract）判定。

行为等价性：在编写代码之前，需要弄清楚spec如何协商形成、如何撰写。

三、规约基本

没规约，没法分派任务，无法写程序；即使写出来，也不知道对错。

（1）规约的优点及作用：

精确的规约，有助于区分责任

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

2、规约可以隔离“变化”，无需通知客户端

3、规约也可以提高编码效率

规约：扮演“防火墙”角色：客户端不需要知道实现，实现者不需要知道如何被使用。

（2）Agreement between an method and its user

什么会达成一致？

1、输入/ 输出的数据类型

2、Functionality and correctness expectations  功能和正确性

3、Performance expectations  性能

（3）What the method does, not how it does it 只讲“能做什么”，不讲

“怎么实现”。

 

（4）规约结构

前置条件：对客户端的约束，在使用方法时必须满足的条件。

Precondition , indicated by the keyword requires.(@requires)

后置条件：对开发者的约束，方法结束时必须满足的条件。

Postcondition , indicated by the keyword effects.(@effects)

Exceptional behavior: what it does if precondition violated.

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

亦即“你违约在先，我自然不遵守承诺”。

当前置条件被违反时，说明客户端有bug，尽管实现者没有义务提醒，但可通过快速失败（failing fast）使bug更容易被找到和修复。

（5）java中的规约

静态类型声明是一种规约，可据此进行静态类型检查（static checking） 

方法前的注释也是一种规约，但需人工判定其是否满足。

Parameters are described by @param clauses and results are described by @return and @throws clauses.

Put the preconditions into @param where possible, and postconditions into @return and @throws.

针对后两点解决方式如图：

其中Find a value in a array是方法前注释

 

1. Specifications for mutating methods

  除非在后置条件里声明过，否则方法内部不应该改变输入参数

Virtually all programmers would assume the same thing. Surprise mutations lead to terrible bugs.  应尽量遵循此规则，尽量不设计

mutating 的spec ，否则就容易引发bugs 。

Convention  程序员之间应达成的默契：除非spec 必须如此，否则不应修改输入参数

– Mutation is disallowed unless stated otherwise .

– No mutation of the inputs

Mutable objects can make simple specification/contracts very

complex mutable

 程序中可能有很多变量指向同一个可变对象（别名）

To put it in terms of specifications, contracts can’t be enforced in just one place anymore, e.g. between the client of a class and the implementer of a class. 无法强迫类的实现体和客户端不保存可变变量的“别名”，这会让用户觉得不安全。

四、规约的比较

如何比较两个规约，以判断是否可以用一个规约替换另一个？

规约的强度S2 >=S1 A specification S2 is stronger than or equal to a specification S1  

1、前置条件更弱

2、for the states that satisfy S1’s precondition，后置条件更强

就可以用S2替代S1

▪ Rules:

– Weaken the precondition: placing fewer demands on a client will never upset

them. 更少的要求

– Strengthen the post-condition, which means making more promises.  更多的承诺

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

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

五、Diagramming specifications

某个具体实现，若满足规约，则落在其范围内；否则，在其之外。

 

程序员可以在规约的范围内自由选择实现方式

客户端无需了解具体使用了哪个实现

更强的规约，表达为更小的区域

更强的后置条件意味着实现的自由度更低了

➔在图中的面积更小

更弱的前置条件意味着实现时要处理更多的可能输入，实现的自由度低了

➔面积更小

 

六、好的规约

  一个好的“方法” 设计，并不是你的代码写的多么好，而是你对该方

法的spec设计的如何。

一方面：client用着舒服。

另一方面：开发者编着舒服。

（一）The specification should be coherent (内聚的)

Spec描述的功能应单一、简单、易理解

• The results of a call should be informative（信息丰富的）

不能让客户端产生理解的歧义

 

▪ If null is returned, you can’t tell whether the key was not bound

previously, or whether it was in fact bound to null.

▪ This is not a very good design, because the return value is useless

unless you know for sure that you didn’t insert null.

一旦返回null ，无法判断是key 不存在对应值，还是key 对应的值就是

null ，不好的设计( 除非确保不会insert null)

• The specification should be strong enough

太弱的spec ，client 不放心、不敢用 ( 因为没有给出足够的承诺) 。

开发者应尽可能考虑各种特殊情况，在post-condition 给出处理措施。

• The specification should also be weak enough

打开什么文件？不知道，所以要考虑多种情况

太强的spec ，在很多特殊情况下难以达到，给开发者增加了实现的难

度（client 当然非常高兴）。

• 在规约里使用抽象类型

可以给方法的实现体与客户端更大的自由度

小结：

一个好的spec应该是内聚的即只做一件事，并且有足够的信息不让客户端产生歧义，强度也要适中，以防过强难以开发&过弱使客户端难以使用。

• 检查前置条件和后置条件

  客户端不喜欢太强的

precondition ，不满足precondition 的输入会导致失败。

惯用做法是：

不限定太强的precondition，而是在postcondition中抛出异常：输入不合法

尽可能在错误的根源处fail，避免其大规模扩散。

是否使用前置条件取决于(1) check的代价；(2) 方法的使用范围

– 如果只在类的内部使用该方法(private)，那么可以使用前置条件(方法内部

不需要判断输入是否满足，认为client会保证前置条件)，在使用该方法的各

个位置进行check——责任交给内部client；

– 如果在其他地方使用该方法(public)，那么可以不使用/放松前置条件(在方

法内部检查输入是否满足)，若client端不满足则方法抛出异常。