设计规约

概述：方法的规约、前置/后置条件、操作式规约、规约的强度及其比较、如何设计好的规约

 

一个完整的方法

• 一个完整的方法包括规约spec和实现体implementation；
• "方法"是程序的积木，它可以被独立的开发、测试、复用；
• 使用“方法”的客户端，无需了解方法内部如何工作，这就是抽象的概念；
• 参数类型和返回值类型的检查都是在静态类型检查阶段完成的。

什么是规约，为什么需要规约

 

• 为什么要有设计规约
  • 很多bug来自于双方之间的误解；没有规约，那么不同开发者的理解就可能不同
  • 代码惯例增加了软件包的可读性，使工程师们更快、更完整的理解软件
  • 可以帮助程序员养成良好的编程习惯，提高代码质量
  • 没有规约，难以定位错误
• 使用设计规约的好处
  • 规约起到了契约的作用。代表着程序与客户端之间达成的一致；客户端无需阅读调用函数的代码，只需理解spec即可。
  • 精确的规约，有助于区分责任，给“供需双方”确定了责任，在调用的时候双方都要遵守。

 

 行为等价性

站在客户端视角看行为等价性

下面给出两个函数

 

static int findFirst(int[] arr, int val) {
    for (int i = 0; i < arr.length; i++) {
        if (arr[i] == val) return i;
    }
    return arr.length;
}

static int findLast(int[] arr, int val) {
    for (int i = arr.length - 1 ; i >= 0; i--) {
        if (arr[i] == val) return i;
    }
    return -1;
}

行为等价性分析：

当val不存在时，findFirst返回arr的长度，findLast返回-1;

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

但是，当val恰好出现在数组的一个索引处时，这两个方法表现相同。

故，如果调用方法时，都传入一个 正好具有一个val的arr ，那么这两种方法是一样的。

总结:1）单纯的看实现代码，并不足以判定不同的实现是否是行为等价的，2）需要根据代码的spec判断行为等价性，3）在编写代码之前，需要弄清楚spec如何协商形成、如何撰写

 

规约的结构：前置条件和后置条件

前置条件（requires修饰）:对客户端的约束，在使用方法时必须满足的条件 

后置条件（effects修饰）：对开发者的约束，方法结束时必须满足的条件 

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

 

例如下面的函数规约：

如果arr为空，可以返回空也可以抛出异常。如果val在arr中出现两次，那么也会抛出异常。

 

静态类型声明是一种规约，可据此进行静态类型检查。

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

参数有@param描述

子句和结果用 @return 和 @ throws子句 描述

尽可能的将前置条件放在 @param 中

 尽可能的将后置条件放在 @return 和 @throws 中

 

 

 可变方法的规约

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

应尽量遵循此规则，尽量不设计 mutating的spec，否则就容易引发bugs。 

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

尽量避免使用可变(mutable)的对象 。

 

 规约的评价

包含以下三个方面：规约的确定性、规约的陈述性以及规约的强度

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

如果S2>=S1,那么

1）前置条件更弱2）后置条件更强

那么这样S2就可以替代S1

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

下面举个例子：

 

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

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

非确定的规约：同一个输入， 多次执行时得到的输出可能不同 （欠定的规约通常有确定的实现）

 

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

声明式规约：没有内部实现的描述，只有 “初-终”状态 

内部实现的细节不在规约里呈现，放在 代码实现体内部注释里呈现。

 

如何设计一个好的规约

规约应该是简洁的：整洁，具有良好的结构，易于理解。

规约应该是内聚的：Spec描述的功能应单一、简单、易理解。

规约应该是信息丰富的：不能让客户端产生理解的歧义。

规约应该是强度足够的：需要满足客户端基本需求，也必须考虑特殊情况。

规约的强度也不能太强：太强的spec，在很多特殊情况下难以达到。

规约应该使用抽象类型：在规约里使用抽象类型，可以给方法的实现体与客户端更大的*度。