羿先生的学习笔记[6]: 规约(Specification)

一、什么是规约

软件设计中的规约(Specification)，指明了某个方法要求的输入及产生的影响。
规约是程序与客户端之间达成的一种契约：使用者有义务按照规约的要求输入数据，程序对正确输入的数据应进行正确的处理。使用者和程序都有义务遵循规约。
规约据此可以分为两部分：前置条件(pre-condition)和后置条件(post-condition)。前置条件是对客户端的约束，是使用方法时必须满足的条件；后置条件是对开发者的约束，是方法结束时必须满足的条件。
使用者在使用方法时，不必关心方法的具体实现，只需阅读规约便可以理解方法的作用。

二、如何写规约

我们以下面这个方法为例：

public static int find(int[] arr, int val)
requires: val occurs exactly once in arr
effects: return index i such that arr[i] = val

方法在arr数组中找到val值并返回val值的索引，要求val在数组中仅出现一次。
我们用注释的方式格式化地给出规约：

 /*** Find a value in an array* @param arr array to search, requires that val occurs exactly once in arr* @param val value to search for* @return index i such that arr[i] = val* @throws NumberException if val does not occur or occurs more than once in arr*/public static int find(int[] arr, int val) throws NumberException{//some code here}

即：

给出方法的功能
用@param表示输入的参数，给出参数的含义
用@return表示返回值的含义
用@throws表示抛出异常对应的情况

这一规约格式可在IDEA等编译器中，在方法前输入 /** ，按回车换行即可自动生成。

三、规约的强弱

我们作为方法的调用者时，能否通过两个方法的规约来判断是否可以调用某一个方法替换另一个方法？这就涉及到了规约的强弱比较：
一个规约A比另一个规约B更强，表示A比B具有更弱的前置条件和更强的后置条件。
例如：

是一个原始的规约

是更强的一个规约，因为其减弱了前置条件。

是一个更强一些的规约，因为其加强了后置条件。
越强的规约，意味着开发者的自由度和责任越重，而使用者的责任越轻。
我们还可以用图形象地表示规约的强弱关系：

越强的规约，在图中所占的面积越小。如果一个规约A在图中所占区域完全被另一个规约B包含，就表示A比B更强。