MIT_6.031之设计规范

1. 目标

理解确定性与不确定性规范，并能够识别和评估其中的不确定性。
理解声明性规范与操作规范，并能够编写声明性规范。
理解前提条件、后置条件及规范的强度，能够比较不同规范的强度。
能够编写出强度适当、连贯有用的规范。

2. 确定性与不确定性规范

确定性规范
- 当满足前提条件时，规范的行为结果是完全确定的。
- 例如：
  1
  2
  3
  static int findExactlyOne(int[] arr, int val)
  requires: val 在数组 arr 中只出现一次
  effects: 返回 arr[i] = val 的索引 i
  - 在这种情况下，输入符合前提条件时，只有一个可能的输出。
不确定性规范
- 允许同样的输入产生多个有效输出，即结果不确定。
- 例如：
  1
  2
  3
  static int findOneOrMoreAnyIndex(int[] arr, int val)
  requires: val 至少在 arr 中出现一次
  effects: 返回 arr[i] = val 的任一索引 i
  - 在这种规范下，同一输入可以有不同的返回结果，具体返回哪个索引取决于实现。
不确定性代码的场景
- 当代码的行为依赖于随机数、并发进程的执行时，不确定性可能会出现。

3. 声明性规范与操作规范

声明性规范
- 不提供中间执行步骤的细节，只描述输入和最终输出的关系。
- 优点：
  - 更加易于理解。
  - 不会暴露不必要的实现细节，避免用户依赖这些细节。
- 示例：
  1
  2
  3
  static int findExactlyOne(int[] arr, int val)
  requires: val 在数组 arr 中只出现一次
  effects: 返回 arr[i] = val 的索引 i
操作规范
- 描述了一系列执行步骤，详细说明了方法是如何操作的。
- 不推荐：它会泄露太多实现细节，使规范难以理解和维护。
- 示例（不推荐）：
  1
  2
  3
  4
  5
  6
  7
  static int findExactlyOne(int[] arr, int val)
  // 操作规范
  for (int i = 0; i < arr.length; i++) {
  if (arr[i] == val) {
  return i;
  }
  }

4. 修改规范的方法

如何判断用新规范替换旧规范是否安全？
- 规范 2 比规范 1 强？
  - 强规范：前置条件更弱，后置条件更强。
  - 如果规范 2 比规范 1 强，那么替换是安全的。
- 可以削弱前置条件：减少对客户的要求不会让他们感到不满。
- 可以增强后置条件：对结果做出更多承诺。

示例：修改前置条件和后置条件

原规范：

1
2
3

static int findExactlyOne(int[] a, int val)
requires: val 在数组 a 中只出现一次
effects: 返回 a[i] = val 的索引 i

弱化前置条件：

1
2
3

static int findOneOrMoreAnyIndex(int[] a, int val)
requires: val 至少在 a 中出现一次
effects: 返回 a[i] = val 的索引 i

增强后置条件：

1
2
3

static int findOneOrMoreFirstIndex(int[] a, int val)
requires: val 至少在 a 中出现一次
effects: 返回 a 中最小的 i, 使得 a[i] = val

5. 设计良好的规范

提前编写规范：在设计方法前，先编写规范有助于清晰思考。
规范应简洁、清晰且结构合理：
- 例如，避免在一个方法中同时进行“计算单词数”和“找到最长的单词”的操作。应将其分解成不同的方法。
返回结果有用：
- 例如，null 作为未找到的返回值并不是一个好的设计，返回无用值会增加客户的困惑。
规范应足够强大：需要给出足够强的保证。
- 例如，如果规范指定处理特殊情况（如异常处理），应保证不会破坏原有的有用方法。
规范应足够弱：
- 例如：
  1
  2
  static File open(String filename)
  effects: 打开名为 filename 的文件
  - 这是一个不好的规范，因为它太强了，没有考虑到文件可能无法打开等实际情况。应修改为“尝试打开文件”。
使用抽象类型：
- 例如：
  1
  static ArrayList<T> reverse(ArrayList<T> list)
  - 这里指定了具体类型 ArrayList，而规范应更通用：
  1
  static List<T> reverse(List<T> list)

6. 是否使用前提条件

前提条件（Preconditions）是指在调用某个方法之前，必须满足的条件。使用前提条件的判断通常取决于以下几个因素：

方法的可见性：
- 公共方法（Public Methods）：
  - 对于公共方法，严格的前提条件可能不太合适，因为这些方法是供外部调用的，调用者可能并不总是了解实现的细节。
  - 如果前提条件过于严格，可能会导致用户在调用方法时频繁遭遇错误或异常，从而影响用户体验。
  - 这种情况下，可以选择在方法内部进行有效性检查，并在发现不符合条件时抛出适当的异常，以提示调用者。
- 私有方法（Private Methods）：
  - 私有方法是仅供类内部使用的，因此可以使用更严格的前提条件。
  - 因为在同一个类中，方法的实现者可以确保在调用私有方法之前已经处理好所有必要的条件。
  - 这种方式可以提高代码的健壮性，确保类的内部逻辑正确。
方法的复杂性：
- 对于复杂的方法，合理设置前提条件可以帮助确保方法在执行时的安全性。例如，若方法涉及多个参数，使用前提条件可以有效减少出错的可能性。
- 复杂方法的前提条件应尽量简单明了，以便于调用者理解。
业务需求：
- 在某些情况下，业务逻辑可能要求在方法执行前必须满足特定条件。例如，在处理用户输入时，确保输入数据的有效性是必要的。
- 这时可以利用前提条件明确要求输入的有效性，从而降低程序出错的概率。
性能考虑：
- 检查前提条件可能会增加一些运行时开销。在性能敏感的场景中，过多的前提条件检查可能会影响程序的性能。
- 需要在安全性与性能之间找到平衡，合理设置前提条件的数量与复杂度。
文档化：
- 前提条件的使用可以作为方法文档的一部分，帮助用户理解方法的使用约束。良好的文档能够减少用户的误用，避免因不当使用造成的错误。
- 清晰的前提条件有助于维护团队的协作，使得其他开发者能够快速理解方法的使用限制。
异常处理：
- 如果决定使用前提条件，应合理处理违反前提条件的情况，通常通过抛出异常来处理不满足条件的调用。
- 提供详细的异常信息可以帮助调用者快速定位问题，并修复相应的错误。

前提条件的使用是一个需要谨慎考量的决策，既要保证方法的安全性和健壮性，又要兼顾用户体验和性能。

7. 访问控制

私有方法（private）有助于保护程序免受错误的影响，避免暴露内部实现细节。

8. 静态方法与实例方法

在面向对象编程中，静态方法（Static Methods）和实例方法（Instance Methods）是两种不同的类型，具有不同的特性和应用场景。以下是它们的详细对比和规范编写方式：

定义与关联性：
- 静态方法：
  - 静态方法是属于类本身的方法，而不是类的具体实例。
  - 这意味着可以在没有创建类实例的情况下调用静态方法，通常通过类名直接调用，如 ClassName.methodName()。
  - 由于静态方法与类的任何特定实例无关，因此它们不能直接访问实例变量和实例方法。
- 实例方法：
  - 实例方法是与特定对象实例相关的方法，它们可以直接访问该实例的属性和其他实例方法。
  - 必须通过创建类的实例来调用实例方法，如 instance.methodName()。
  - 实例方法在其操作中可能依赖于实例的状态，因此可以进行更复杂的逻辑处理。
规范编写：
- 静态方法规范：
  - 在编写静态方法的规范时，应明确其前置条件和后置条件，说明在调用该方法前需要满足的条件，以及调用后所期望的结果。
  - 由于静态方法不涉及实例状态，前置条件通常与方法参数直接相关，例如：
    1
    2
    3
    static int calculateSum(int a, int b)
    requires: a >= 0 && b >= 0
    effects: returns the sum of a and b
  - 后置条件应明确结果的性质和类型，例如返回值的有效性和范围。
- 实例方法规范：
  - 实例方法的规范同样需要明确前置条件和后置条件，但这些条件通常会涉及到对象的状态。
  - 在前置条件中，可以要求特定的实例属性满足某些条件，例如：
    1
    2
    3
    4
    5
    6
    7
    8
    class Account {
    private double balance;
    
    // 实例方法
    public void deposit(double amount)
    requires: amount > 0
    effects: increases the balance by amount
    }
  - 后置条件通常涉及到实例的状态变化，例如余额的更新、状态的改变等。
设计考虑：
- 静态方法：
  - 静态方法适用于那些不依赖于实例状态的功能，例如工具类方法、工厂方法等。
  - 编写静态方法时，可以利用它的独立性进行更简洁的设计，但需注意在方法中处理错误和异常，以确保调用的安全性。
- 实例方法：
  - 实例方法适用于需要操作对象内部状态的情形，能够反映出实例间的差异。
  - 编写实例方法的规范时，考虑到方法可能会修改实例的状态，确保后置条件能够准确反映这些变化至关重要。
使用场景：
- 静态方法常用于提供不依赖于类实例的通用功能，例如计算、转换等。实例方法则用于需要对对象的特定状态进行操作的场合，如业务逻辑、数据处理等。