第三章第二节 软件规约

　　这一节我们转向关注“方法/函数/操作”是如何定义的，即讨论编程中的动词，规约。

Outline

• 一个完整的方法
• 什么是设计规约，我们为什么需要他
• 行为等价性
• 规约的结构：前置条件与后置条件
  • 规约的结构
  • 可变方法的规约
• 规约的评价
  • 规约的确定性
  • 规约的陈述性
  • 规约的强度
  • 如何设计一个好的规约
  • 是否使用前置条件

Notes

## 一个完整的方法

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

## 什么是设计规约，我们为什么需要他

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

## 行为等价性

行为等价性就是站在客户端的角度考量两个方法是否可以互换

参考下述两个函数：

 1 static int findFirst(int[] arr, int val) {
 2     for (int i = 0; i < arr.length; i++) {
 3         if (arr[i] == val) return i;
 4     }
 5     return arr.length;
 6 }
 7
 8 static int findLast(int[] arr, int val) {
 9     for (int i = arr.length - 1 ; i >= 0; i--) {
10         if (arr[i] == val) return i;
11     }
12     return -1;
13 }

• 行为等价性分析：
  • 当val不存在时，findFirst返回arr的长度，findLast返回-1;
  • 当val出现两次时，findFirst返回较低的索引，findLast返回较高的索引。
  • 但是，当val恰好出现在数组的一个索引处时，这两个方法表现相同。
  • 故，如果调用方法时，都传入一个 正好具有一个val的arr ，那么这两种方法是一样的。
• 另外，我们也可以根据规约判断是否行为等价注：规约与实现无关，规范无需讨论方法类的局部变量或方法类的私有字段。

  • static int findExactlyOne(int[] arr, int val)
      requires: val occurs exactly once in arr
      effects:  returns index i such that arr[i] = val

  • 两个函数附和同一个规约，故二者等价

## 规约的结构：前置条件与后置条件

【规约的结构】

• 一个方法的规约常由以下几个短句组成契约：如果前置条件满足了，后置条件必须满足。如果没有满足，将产生不确定的异常行为
  • 前置条件(precondition)：对客户端的约束，在使用方法时必须满足的条件。由关键字 requires 表示；
  • 后置条件(postcondition)：对开发者的约束，方法结束时必须满足的条件。由关键字 effects 表示
  • 异常行为(Exceptional behavior)：如果前置条件被违背，会发生什么
• 
• 静态类型声明是一种规约，可据此进行静态类型检查。
• 方法前的注释也是一种规约，但需人工判定其是否满足。
  • 参数由@param 描述
  • 子句和结果用 @return 和 @ throws子句 描述
  • 尽可能的将前置条件放在 @param 中
  • 尽可能的将后置条件放在 @return 和 @throws 中
  • 

【mutating methods(可变方法)的规约】

• 除非在后置条件里声明过，否则方法内部不应该改变输入参数。
• 应尽量遵循此规则，尽量不设计 mutating的spec，否则就容易引发bugs。
• 程序员之间应达成的默契：除非spec必须如此，否则不应修改输入参数 。
• 尽量避免使用可变(mutable)的对象 。
  • 对可变对象的多引用，需要程序维护一致性，此时合同不再是单纯的在用户和实现者之间维持，需要每一个引用者都有良好的习惯，这就使得简单的程序变得复杂；
  • 可变对象使得程序难以理解，也难以保证正确性；
  • 可变数据类型还会导致程序修改变得异常困难；

## 规约的评价

规约评价的三个标准

• 规约的确定性
• 规约的陈述性
• 规约的强度

【规约的确定性】

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

1 static int findExactlyOne(int[] arr, int val)
2   requires: val occurs exactly once in arr
3   effects:  returns index i such that arr[i] = val

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

1 static int findOneOrMore,AnyIndex(int[] arr, int val)
2   requires: val occurs in arr
3   effects:  returns index i such that arr[i] = val

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

【规约的陈述性】

• 操作式规约（Operational specs）：伪代码 。
• 声明式规约（Declarative specs）：没有内部实现的描述，只有 “初-终”状态 。
• 声明式规约更有价值 ； 内部实现的细节不在规约里呈现，而放在代码实现体内部注释里呈现。

举一个栗子：

static String join(String delimiter, String[] elements)
effects : returns the result of adding all elements to a new : StringJoiner(delimiter) // Operational specs

effects:returns the result of looping through elements and alternately appending an element and the delimiter // Operational specs

effects: returns concatenation of elements in order, with delimiter inserted between each pair of adjacent elements // Declarative specs

【规约的强度】

• 通过比较规约的强度来判断是否可以用一个规约替换另一个；
• 如果规约的强度 S2>=S1，就可以用S2代替S1，体现有二：一个更强的规约包括更轻松的前置条件和更严格的后置条件；越强的规约，意味着实现者(implementor)的自由度和责任越重，而客户(client)的责任越轻。
  • S2的前置条件更弱
  • S2的后置条件更强

举一个栗子：

• Original spec：

1 static int findExactlyOne(int[] a, int val)
2   requires: val occurs exactly once in a
3   effects:  returns index i such that a[i] = val

• A stronger spec:

1 static int findOneOrMore,AnyIndex(int[] a, int val)
2   requires: val occurs at least once in a
3   effects:  returns index i such that a[i] = val

• A much stronger spec:

1 static int findOneOrMore,FirstIndex(int[] a, int val)
2   requires: val occurs at least once in a
3   effects:  returns lowest index i such that a[i] = val

【如何设计一个好的规约】

• 规约应该是简洁的：整洁，具有良好的结构，易于理解。
• 规约应该是内聚的：Spec描述的功能应单一、简单、易理解。
• 规约应该是信息丰富的：不能让客户端产生理解的歧义。
• 规约应该是强度足够的：需要满足客户端基本需求，也必须考虑特殊情况。
• 规约的强度也不能太强：太强的spec，在很多特殊情况下难以达到。
• 规约应该使用抽象类型：在规约里使用抽象类型，可以给方法的实现体与客户端更大的自由度。

【是否使用前置条件】

• 是否使用前置条件取决于如果只在类的内部使用该方法(private)，那么可以不使用前置条件，在使用该方法的各个位置进行check——责任交给内部client。
  • check的代价；
  • 方法的使用范围；
• 如果在其他地方使用该方法(public)，那么必须要使用前置条件，若client端不满足则方法抛出异常。

原文地址：https://www.cnblogs.com/hithongming/p/9125628.html