本章说明

本章简单介绍了程序设计语言中函数的基本概念，然后具体介绍了文档与规约。包括规约的前置条件、后置条件，可变数据对其的影响，如何设计规约等。其实就是教给开发者如果通过编写规范的规约更好的保证函数的正确性，防止异常的产生，和用户更好的协作。

正文

一、程序设计语言中的函数&方法

方法、参数、返回值、变量作用域、方法：积木
（主要介绍了函数的基本概念，包括返回值、变量作用域、调用等，较为基础，不做过多解释

二、规约

1、编程中的文档

文档通常包括类层次结构和已实现接口的列表，直接子类，对于接口，实现类，类的描述，构造函数摘要，方法摘要，每个方法和构造函数的详细描述，方法签名：我们看到返回类型、方法名称和参数，参数：方法参数的描述，以及方法返回内容的描述。
（文档的内容、作用以及写文档的重要性

2、规格说明（或者称为契约）

规格说明是团队开发的关键，是分配责任的基础。规格说明是实现者和使用者之间的一种契约，实现者有责任满足契约，使用者可以信赖契约。准确的规格说明利于确定错误的位置和责任，客户端不需要阅读代码，通过说明了解程序。

规格说明给了实现者实现的自由，在保证约定 下，可以自由修改实现。 通过在说明中增加对输入的限定，省略掉耗时的正确性检查工作，提升效率。（保证输入正确性的责任由调用者承担）。

3、行为等价

确定行为的等价， 关键是一个规格说明实现是否可以替换另一个。

这些方法不仅具有不同的代码，而且实际具有不同的行为。但是，当val恰好出现在数组的一个索引处时，这两个方法的行为相同。
等价的判定由调用者视角确定，判定可替代与否，需要对调用端依赖内容的准确描述。注意，规约不应涉及实现的内部变量和私有域。

4、规约结构：前置条件和后置条件

规约结构
前置条件是用户的义务，而后置条件是实现者的义务。规格说明蕴含了以下逻辑：如果前置条件满足了，则后置条件必须满足；反之，如果前置条件不满足，后置条件则无需满足。
Java中的规约
前置和后置条件中对类型的声明，将由编译器进行检查，确保正确性，其余部分通过注释的形式进行描述，由人来保证正确性 。例如：@param、@return

可变方法的规格说明
如果没有明确说明，则默认输入值是不可变的，可变带来巨大的麻烦。通过情况， 除非另有说明，保持不可变 ，不对输入进行修改。
可变对象使简单的契约变复杂
对可变对象的多引用，需要程序维护其一致性。此时约定不再是单纯的在调用者和实现者之间维持， 需要程序中每处的对其调用都有良好的行为 。可变使对象具有全局属性，导致难于理解和确保正确性。可变的优点是性能和便利，但是需要额外的确保无措的成本。
可变对象降低了可变性
可变对象使调用者和实现者的规约更加复杂，降低了双方修改的自由。
例如实现者为了提高运行速度为数据库中内容加入了缓存，如果是可变对象有可能被用户修改。可以在规约里警告用户。

下面这个规格说明至少说明了数组会被更改，但此类说明仍然不能够确保 产生新的别名引用，以及未来的修改。

下面这种修使用了不可变类型String，不依赖于程序员对规格说明的认真对待程度，允许实现者增加实现自由。

5、测试和验证规格说明

正式的规格说明
Java Modelling Language (JML)

文本规格说明-Javadoc

语意正确遵守契约
编译器、静态分析工具可以进行类型检查和错误类型，但无法保证语意正确性。
如果要保证语意正确性：
使用数学方法证明正式规范的正确性
正式证明实现的所有可能执行都符合规范
手工努力; 部分自动化; 不能自动判定
测试
在受控环境中使用所选输入执行程序，或者说根据规格说明来编写测试用例，尽量保证能够实现预计的效果。
黑盒测试
遵循规格说明来进行测试，而无需考虑其内部具体实现细节。

三、设计规约

1、规格说明分类

比较规格说明
确定性: 唯一的输出，还是多个合法的输出；只是单纯的描述输出，还是给出了如何计算输出 ；限制为较少的实现方式，还是较多的实现。
确定与低确定性规格说明
确定性：只有一个返回值和一个最终状态，不存在有效输入对应多个有效输出。

低确定的：允许同一输入存在多个有效输出。

非确定的： 输出结果不确定。
将不是确定性的spec统一定义为underdetermined 欠定的。规格说明的不确定性，为实现者提供了在实现时选择实现方案的机会。一个欠定的规格说明通常是通过完全确定性的实现来实现的。
陈述性和操作性的规格说明
操作性的：为维护人员提供解释，如果必需的话，放到内部的注释中，而不是在spec中。
陈述性的：简短，易于理解，不会暴露内部实现细节。

更强的和更弱的规格说明
如何比较两个规格说明的行为，以决定是否可以进行替换？
如果S2的前置条件更弱，后置条件更强则比S1更强，所以满足S2的实现可以用于满足S1，并且这个替换是安全的。“要求的更少，承诺的更多”。


如果S3既不强也不弱于S1，那么规格可能会重叠（因此存在仅满足S1，仅满足S3，S1和S3的实现）或者可能是不相交的。
在这两种情况下，S1和S3都是不可比较的。

2、图表规约

每个点代表一个实现，一个规格说明定义了一个区域，其中包含的点为其实现。一个实现或者满足规格说明(区域内)，或者不满足(区域外)。
当S2强于S1时，它在该图中定义了一个较小的区域; 较弱的规范定义了一个更大的区域。
加强后置条件，意味着对输出要求更多，实现自由变少 。 弱化前置条件，实现中需要处理更多的情况。
上述两点使可满足的实现变少(点变少)，故规格说明越强，区域越小。

3、设计好的规格说明

规格说明的质量
设计一个方法的首要任务是编写规格说明，没有通用的准则，但存在一些有用的指导。
规格说明应该是内聚的
规范不应该有很多不同的情况。 长参数列表，深层嵌套的if语句和布尔标志都是麻烦的标志。

举个例子，上面这段代码同时做了两件事，应该分到两个方法中，易于理解，同时易于改变。
调用的结果应该提供信息

如果返回null，则无法判断key是否先前未绑定，或者是否实际上绑定为null。
这不是一个非常好的设计，因为除非确定没有插入null，否则返回值是无用的。
规格说明应该足够强
确保通常情况的正确处理，同时也要对异常情况格外关注。对不合理参数进行抛出异常处理后，不要允许随意的修改，否则会导致调用者不清楚实际发生了什么。
规格说明也应该足够弱

这个例子首先缺少重要的细节，比如这个文件打开后是用来读还是写。另外这个规格说明太强了，因为它无法保证打开文件。 它运行的过程可能缺少打开文件的权限，或者文件系统可能存在一些超出程序控制范围的问题。所以这个规格说明应该弱一些，比如“尝试打开一个文件”。
规格说明应该使用抽象类型
例如用List或Set而不是ArrayList或HashSet，这样会给用户和实现者提供更大的自由。由于规范的行为不依赖于有关ArrayList的任何特定内容，因此最好根据更抽象的List来编写此规范。
前置条件还是后置条件？
对于编程人员：检查条件的正确性代价很高时，应该通过前置条件处理。
对于用户： Java API类倾向于采用后置条件的方式处理，当参数不合适时它们会抛出未检查异常。 找到由传递的错误参数引起的bug更加容易。 快速失败是好的决策，使失败点离bug尽可能的近，易于定位。
选择前置或后置的关键因素是检查的代价以及方法的作用范围。 如仅在类的内部调用，则可以通过仔细检查调用该方法的所有位置来确保前提条件的满足 。如果是public的方法，则适宜采用后置条件(抛出异常) 。