文档

规格说明 specification¶

客户不再需要通过阅读复杂代码了解功能，实现者也可以更加自由的编写代码；

规格说明的格式

/**
     * Get the next element of the list.
     * Requires: hasNext() returns true.
     * Modifies: this iterator to advance it to the element 
     *           following the returned element.
     * @param list list to iterate over
     * @return next element of the list
     * @throws NoSuchUserException if nobody with username is in MIT's database
     */

规格说明的内容¶

前置条件 precondition
- 在调用方法前需要成立的条件，比如输入参数的要求
后置条件 postcondition
- 方法执行之后将会成立的条件，给出对期望结果的保证，不如对返回值的保证
如果调用方法时前提条件成立，那么方法完成时后置条件也必须成立。
避免使用 null，通常应该禁止 null 参数或 null 返回值，如果需要使用 null 应该在说明中明确指出
默认不会对输入的参数进行修改（函数的副作用），如果需要更改，应该明确指出
不需要包含内部变量、实现等内部自身的内容

Javadoc

/**
 * 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
 */
static int find(int[] arr, int val)

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

int[] array = new int[] { 7, 7, 7 };
assertEquals(0, find(array, 7));  // bad test case: violates the spec
assertEquals(7, array[find(array, 7)]);  // correct

^f74bca - 并没有说明有多个匹配时的返回规则，不能自己进行假定，测试要按照规则严格制定 - 同时，先决条件说了一定在 arr 中出现 val，因此也不需要测试不存在的情况

规格说明的性质¶

决定性（Deterministic）：规范是否仅为给定输入定义了唯一的可能输出，或者允许实现者从一组合法的输出中进行选择？
- 如果规范是高度决定性的，那么对于相同的输入，它将有一致的、唯一的输出。
- 如果规范具有一定的非决定性（underdetermined），那么对于相同的输入，可能有多个合法的输出。（并不是说每次输入，结果会发生变化，就像使用了随机数，而只是说不能通过输入预判一个确定的结果，有多个结果都可以作为合法的输出，这取决于具体的实现）

比如对于在数组中查找元素

//只出现一次，返回值确定，为决定性的
static int findExactlyOne(int[] arr, int val)
  requires: val occurs exactly once in arr
  effects:  returns index i such that arr[i] = val
//多次出现，返回值不确定（比如从前向后和从后向前搜索就会得到不同的结果），为非决定性
static int findOneOrMore,AnyIndex(int[] arr, int val)
  requires: val occurs in arr
  effects:  returns index i such that arr[i] = val

声明性（Declarative）：规范是仅描述输出应该是什么，还是明确说明了如何计算输出？
- 声明性规范通常更加抽象，只关注所需的结果，而不涉及实现的细节。
- 明确性 (operational) 规范则提供了实现的详细步骤，以确保结果的生成。（如 pseudocode 伪代码，通常不使用这种类型，因为这会对外暴露内部实现，导致客户使用不想被使用的具体实现细节）
在大部分情况下，不应该在函数的规范说明处解释函数的具体实现细节。这部分注释应该在具体的代码中作为行中的注释
强度（Strength）：规范是否对合法的实现有明确的限制，还是具有广泛的合法实现方式？
- 强规范可能会规定只有一小部分合法实现方式，通常用于对特定问题的严格约束。
- 弱规范则可能会允许更多不同的实现方式，通常用于更灵活的问题。
如何修改方法而不应先原先用户的使用：S2 的规范应该强于修改之前的 S1
- S2 的前置条件不强于 S1
- S2 的后置条件不弱于 S1
图表示
- 圆圈表示规范，内部表示具体实现，圈越小说明条件越强

什么是好的规格说明¶

coherent：连贯一致的，每个说明（函数）应该专注于完成一个任务

/**
 * Update longestWord to be the longest element of words, and print
 * the number of elements with length > LONG_WORD_LENGTH to the console.
 * @param words list to search for long words
 */
public static void countLongWords(List<String> words)

应该考虑把找到最长的单词和筛选划分为两个独立的方法
提供足够的（明确的）信息
- 如返回值 null 表示表示特殊含义，则就应该表示唯一的特殊含义而不应该具有歧义

足够强，为用户提供足够的必要保证

static V put (Map<K,V> map, K key, V val)
  requires: val may be null, and map may contain null values
  effects:  inserts (key, val) into the mapping,
              overriding any existing mapping for key, and
              returns old value for key, unless none,
              in which case it returns null

虽然提到遇到 null 会抛出异常，但是用户不知道已经有哪些元素加入了 list，也就是说用户不知道如何对异常进行处理

足够弱

static File open(String filename)
  effects: opens a file named filename

保证打开文件是不现实的，应该是尝试打开文件等
尽可能使用抽象数据结构（如 List 接口），提供更大的自由度
- 如使用 List 而不是 Arraylist 减少不必要的转换（如果 ArrayList 的特性并不是必须的）
有时应该对输入进行检查（由方法判断前置条件是否得到满足，尽早抛出异常）；而有时应该由调用者自行检查（如二分搜索）。具体何时进行检查由检查的代价，以及应用范围决定。