MIT_6.031之规范

1. 目标与规范的重要性

  • 目标: 通过编写详细、精确的规范，明确每个方法的前置条件和后置条件，进而编写正确的实现与测试。同时理解 Java 中的异常处理，特别是已检查（checked）和未检查（unchecked）异常之间的区别。

  • 为什么要规范:

    • 责任分摊: 规范明确了客户与实现者之间的责任，客户需要满足前提条件，实施者则保证提供预期的后置效果。
    • 降低复杂性: 精确的规范省去了阅读代码的负担，使得使用者可以通过理解规范进行调用，而无需关心实现细节。
    • 独立修改: 实现者在保证满足规范的前提下，可以自由更改代码的内部实现，而不影响使用者。

2. 方法规范的组成

  • 先决条件 (Preconditions): 表明调用方法前必须满足的条件。常通过 requires 子句来定义。例如：

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

  • 后置条件 (Postconditions): 表示在满足先决条件的情况下，方法执行后应保证的结果。常通过 effects 子句来定义。例如：

    1
    2
    static int find(int[] arr, int val)
      effects: returns index i such that arr[i] = val

  • 快速失败原则: 如果不满足前置条件，理想情况下应抛出异常而不是继续执行。这有助于尽早发现问题，避免错误传播。

3. 编写方法的 Java 规范

Java 提供了文档注释用于编写方法的规范，通常通过 @param, @return, @throws 等标签进行描述。

  • 参数规范 (@param): 描述方法的参数及其要求。
  • 返回值规范 (@return): 描述方法的返回值以及后置条件。
  • 异常规范 (@throws): 描述可能抛出的异常及其情况。

示例：find 方法的 Java 规范

1
2
3
4
5
6
7
8
9
10
/**
 * 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 IllegalArgumentException if val occurs more than once or not at all
 */
static int find(int[] arr, int val) {
    // 实现细节
}

4. 处理空引用

  • 基本类型：不能为 null，例如 int、double 等。它们在声明时必须初始化。

    1
    2
    int size = null;     // 错误
    double depth = null; // 错误

  • 非基本类型：如 String、List 等，可以为 null，但访问它们的方法或属性可能会抛出 NullPointerException。

    1
    2
    String name = null;
    name.length();  // 抛出 NullPointerException

  • 避免空引用：推荐在规范中使用诸如 @NonNull 注解来隐式禁止参数或返回值为 null。

    1
    2
    3
    static boolean addAll(@NonNull List<T> list1, @NonNull List<T> list2) {
        // 实现细节
    }

5. 测试遵循规范

  • 单一关注点: 一个良好的单元测试应专注于单个规范，不应做超出规范的假设。例如，测试某个 find 方法时，只需验证其返回结果是否符合 val 在数组中唯一存在的要求。

6. Java 异常机制

Java 的异常机制可以帮助程序员处理错误和特殊情况。异常分为已检查异常和未检查异常，它们适用于不同的场景。

6.1 已检查异常 (Checked Exceptions)

  • 已检查异常用于表示方法的特殊结果或预期的错误。必须在方法签名中声明，并由调用方处理。

    1
    2
    3
    4
    LocalDate lookup(String name) throws NotFoundException {
        // 如果找不到，抛出 NotFoundException
        throw new NotFoundException();
    }

  • 调用方必须使用 try-catch 块捕获或在其方法上声明异常：

    1
    2
    3
    4
    5
    try {
        LocalDate date = lookup("Alice");
    } catch (NotFoundException e) {
        // 处理异常
    }

6.2 未检查异常 (Unchecked Exceptions)

  • 未检查异常通常表示编程错误或系统错误，如 NullPointerException、ArrayIndexOutOfBoundsException 等。它们不需要在方法签名中声明。

    1
    2
    String name = null;
    name.length();  // 抛出 NullPointerException

  • 程序员可以使用 RuntimeException 来创建自定义的未检查异常：

    1
    2
    3
    4
    5
    class MyCustomException extends RuntimeException {
        public MyCustomException(String message) {
            super(message);
        }
    }

7. Java 异常的类层次结构

  • Throwable: 是所有异常的基类。它有两个主要子类：Error 和 Exception。
    • Error: 表示严重的系统错误，如 StackOverflowError、OutOfMemoryError，通常不可恢复。
    • Exception: 大部分应用程序的异常。RuntimeException 是它的子类，表示未检查异常。
1
2
3
4
5
Throwable
   ├── Error (unchecked)
   └── Exception
       ├── RuntimeException (unchecked)
       └── OtherCheckedExceptions (checked)

8. 异常设计注意事项

  • 使用已检查异常处理特殊结果: 对于需要显式处理的情况，使用已检查异常。

  • 使用未检查异常检测错误和意外情况: 程序中的编程错误，如数组越界、空指针等，通常使用未检查异常。

  • 避免滥用异常: 不要使用异常进行正常控制流程。以下代码效率低下：

    1
    2
    3
    4
    5
    6
    try {
        int i = 0;
        while (true) {
            a[i++].f();
        }
    } catch (ArrayIndexOutOfBoundsException e) { }

    替代方案是使用标准循环：

    1
    2
    3
    for (int i = 0; i < a.length; i++) {
        a[i].f();
    }

9. 总结

  • 安全性: 一个好的规范能准确记录双方（客户与实现者）所依赖的假设，减少错误。
  • 简明性: 规范应该尽量简短，便于理解，且减少代码阅读的负担。
  • 灵活性: 在保证规范的前提下，允许自由修改代码实现。

在使用 Java 的文档注释和异常机制时，牢记规范的目的，确保方法实现与调用者之间的相互契约清晰且有效。