methodical-programming

方法化编程（Programación Metódica）

应用严谨且以数学为基础的程序构造与验证技术。程序应根据形式化规格推导得出，而不是临时编写后再进行测试。这项技能与编程语言无关，适用于任何编程范式。

核心原则

1. 先写规格，再写代码

每个函数/过程都必须包含以下规格：

• 前置条件（Pre）： 输入必须满足的条件。
• 后置条件（Post）： 输入与输出之间必须成立的关系。

function f(params) returns results
  {Pre: conditions on params}
  {Post: relations between params and results}

当程序的实际行为符合其规格时，该程序就是正确的。前置条件越弱，函数的可复用性越强。后置条件越强，函数的实用性越高。

2. 推导优先于验证

• 验证： 证明现有程序符合其规格（事后进行）。
• 推导： 根据规格构造一个从构造上就正确的程序。

始终优先选择推导。根据后置条件分析推导代码：

• 程序变量与表达式之间的等式 → 通过赋值求解。
• 后置条件中的析取 → 设计备选方案/条件分支（if/match/switch）。
• 后置条件中的合取 → 尝试顺序组合或条件分支。

3. 状态、断言与替换

• 状态是程序在某个位置上所有变量当前值的映射。
• **断言（aserto）**是关于程序变量的逻辑表达式，用于描述一组有效状态。
• 替换 A[x ← E]：将断言 A 中每个自由出现的 x 替换为表达式 E。这是对赋值进行推理的关键操作。

---

指令语义（公理化）

无论语言语法如何，都应用这些规则。

跳过 / 空操作

{A} skip {A}

操作前成立的一切，操作后仍然成立。

赋值

{A[x ← E]} x := E {A}

要证明 {P} x := E {Q}，需证明：

1. 表达式 E 可以无错误地求值。
2. P ⟹ Q[x ← E]（前置条件蕴含将 x 替换为 E 后的后置条件）。

多重赋值（同时赋值）

<x₁, x₂, ..., xₙ> := <E₁, E₂, ..., Eₙ>

所有表达式都使用赋值之前的值求值。当变量出现在右侧表达式中时，这一点尤为重要。

顺序组合

{A₁} P₁ ; P₂ {A₃}

找到一个中间断言 A₂，使得 {A₁} P₁ {A₂} 且 {A₂} P₂ {A₃}。

条件 / 备选方案

{Pre}
if B₁ → S₁
   B₂ → S₂
   ...
   Bₙ → Sₙ
end if
{Post}

验证：

1. 完备性： Pre ⟹ B₁ ∨ B₂ ∨ ... ∨ Bₙ（至少有一个分支可执行）。
2. 每个分支的正确性： 对每个 i，均有 {Pre ∧ Bᵢ} Sᵢ {Post}。

函数调用

<x₁, ..., xₘ> := f(e₁, ..., eₖ)

1. 调用前：证明实参满足函数的前置条件。
2. 调用后：结果变量满足后置条件（并进行参数/结果重命名）。

---

量词与隐藏操作

使用量词简洁地表达规格。每个量词都有一个中性元素（空定义域上的取值）：

量词	符号	中性元素	类型	描述
求和	Σ	0	数值	对定义域求和
求积	Π	1	数值	对定义域求积
全称量词	∀	true	布尔	对定义域进行合取（与）
存在量词	∃	false	布尔	对定义域进行析取（或）
计数器	N	0	自然数	统计谓词成立的数量
最大值	MAX	—	数值	定义域中的最大值
最小值	MIN	—	数值	定义域中的最小值

拆分量词——从定义域中分离一个元素，并与二元运算组合：

Σ(a: 1≤a≤n: f(a)) = Σ(a: 1≤a≤n-1: f(a)) + f(n)
MAX(a: 1≤a≤n: f(a)) = max(MAX(a: 1≤a≤n-1: f(a)), f(n))

中性元素定义了递归的基本情况和迭代的初始化值。

---

代数数据类型

使用数据类型时，请根据其代数规范进行推理：

1. 签名： 类型（属）以及带有元数的运算。
2. 等式： 定义运算行为的代数恒等式。
3. 构造子： 能构造该类型任意值的最小运算集合（用作归纳的基础）。

常见结构

列表： 构造子 []（空列表）和 e:l（cons）。运算：++（拼接）、length。

[] ++ l₂ ≡ l₂
(e:l₁) ++ l₂ ≡ e:(l₁ ++ l₂)
length([]) ≡ 0
length(e:l) ≡ 1 + length(l)

栈（LIFO）： 构造子 empty_stack 和 push(e, s)。运算：top、pop、is_empty。

top(empty_stack) ≡ error
top(push(e, s)) ≡ e
pop(push(e, s)) ≡ s
is_empty(empty_stack) ≡ true
is_empty(push(e, s)) ≡ false

队列（FIFO）： 构造子 empty_queue 和 enqueue(e, q)。运算：front、dequeue、is_empty。

二叉树： 构造子 empty_tree 和 plant(e, left, right)。运算：root、left、right、is_empty、height、size。

height(empty_tree) ≡ 0
height(plant(e, a₁, a₂)) ≡ 1 + max(height(a₁), height(a₂))
size(plant(e, a₁, a₂)) ≡ 1 + size(a₁) + size(a₂)

表/映射： 构造子 create 和 assign(t, index, value)。运算：lookup、defined。

使用构造子集合来确定每种类型的归纳结构。

---

归纳原理

要证明数据类型的性质，请找出其构造子，并使用结构归纳法进行推理：

[P(base) ∧ ∀x (P(smaller(x)) ⟹ P(x))] ⟹ ∀z P(z)

• 基础情况： 证明由零元构造子构造的值（空列表、空栈等）满足该性质。
• 归纳步骤： 假设所有子结构都满足该性质，并证明组合结构也满足该性质。

需要一个良基预序（noetherian）：不存在无限严格递减序列。这能保证归纳和递归终止。

---

递归程序

模式

每个递归函数都遵循以下结构：

function f(x) returns r
  {Pre: Q(x)}
  if d(x) →          // direct case
    r := h(x)
  ¬d(x) →            // recursive case
    v := f(s(x))
    r := c(x, v)
  end if
  {Post: R(x, r)}
  return r

验证步骤

1. 直接情况的正确性： Q(x) ∧ d(x) ⟹ R(x, h(x))
2. 递归情况——调用合法： Q(x) ∧ ¬d(x) ⟹ Q(s(x))（递归实参满足前置条件）
3. 递归情况——正确性： Q(x) ∧ ¬d(x) ∧ R(s(x), v) ⟹ R(x, c(x, v))
4. 界函数 t(x)： 定义 t: params → ℕ，使得：
   • Q(x) ⟹ t(x) ∈ ℕ（始终为自然数）
   • Q(x) ∧ ¬d(x) ⟹ t(s(x)) < t(x)（每次递归调用时都严格递减）

界函数启发式

参数类型	常见界函数
递减的自然数 n	n 本身
两个自然数，其中一个始终递减	m + n
两个自然数，其中一个递减，另一个增长但始终不达到它	max(m, n)
布尔值 b 从 true → false 变化	if b then 1 else 0
布尔值 b 从 false → true 变化	1 - (if b then 1 else 0)
栈	height(stack)
队列	length(queue)
二叉树	size(tree) 或 height(tree)
列表	length(list)
收缩的区间 [i, j]	j - i

递归类型

• 线性递归： 每次调用至多产生一次递归调用。
• 多重递归： 一次调用可能产生多个递归调用（例如，树遍历）。

递归程序设计方法

1. 指定函数：函数头、前置条件、后置条件。
2. 确定界函数 t(x)——用于在 ℕ 上进行归纳的表达式。
3. 分析情况： 找出至少一个直接情况和一个递归情况。确保覆盖所有情况。
4. 编写程序并验证每种情况。 对于递归情况，假设（根据归纳假设）递归调用满足规范。
5. 验证终止性： 证明每次递归调用时 t(x) 都严格递减。

---

算法沉浸（泛化）

如果找不到直接的递归解法、解法效率不高或难以推理，请通过增加参数和/或结果来泛化函数。这称为沉浸。

技术

强化前置条件

1. 弱化后置条件（可以引入新变量）。
2. 用弱化后的后置条件强化前置条件——要求输入中包含结果的部分版本。
3. 添加浸入参数，使新的前置条件合理。
4. 保留原后置条件。

弱化后的后置条件可为以下内容提供思路：

• 基本情况守卫：用于“反转”弱化的条件。
• 递归情况：各次调用之间只有浸入参数发生变化 → 具有恒定后置条件的尾递归。

弱化后置条件

1. 引入新变量，替换后置条件中的子表达式。
2. 删除部分等式 → 降低要求。
3. 被删除的等式变为初始化，用于从浸入中恢复原函数。
4. 根据需要，用新参数的定义域条件强化前置条件。

效率浸入

当复杂表达式 f(x) 必须在每次递归调用时重新计算时：

• 作为额外结果：在后置条件中添加 w = f(x)。在以 s(x) 进行递归调用后，将 w 从 f(s(x)) 更新为 f(x)。
• 作为额外参数：在前置条件中添加 w = f(x)。使用 w，而不是计算 f(x)。进行递归调用时，根据当前的 w 计算新的参数值。

展开/折叠技巧（尾递归转换）

将线性递归转换为尾递归：

1. 给定 f(x) = c(f(s(x)), x)（线性递归情况），定义浸入 g(y, w) = c(f(y), w)。
2. 展开：将 f 的各个情况代入 g 的定义。
3. 折叠：调整表达式，使其回到 g 的形式。
4. 得到尾递归函数 g，且 f(x) = g(x, neutral)，其中 neutral 是 c 的单位元。

---

迭代程序（循环）

While 循环语义

{Invariant I}
while B do
  S
end while
{Post: Q}

验证（两个阶段）

阶段 1 — 部分正确性：

1. 定义一个不变式 I：每次迭代开始时都成立的条件。
2. 初始化：Pre ⟹ I（前置条件蕴含不变式）。
3. 保持：{I ∧ B} S {I}（循环体保持不变式）。
4. 退出：I ∧ ¬B ⟹ Post（不变式 + 循环退出条件蕴含后置条件）。

阶段 2 — 终止性：

1. 定义一个取值在 ℕ 中的界函数 t。
2. 有界：I ∧ B ⟹ t > 0。
3. 递减：{I ∧ B ∧ t = T} S {t < T}（循环体严格减小界）。

转换：尾递归 → 迭代

具有恒定后置条件的尾递归函数可直接转换为 while 循环：

递归元素	迭代元素
浸入函数的前置条件	循环不变式
界函数（前序）	循环界函数
浸入参数	循环局部变量
递归情况守卫	循环条件 B
递归调用中的参数更新	循环循环体
直接情况的循环体	循环之后的代码
初始调用参数	循环初始化（while 之前）

直接推导迭代程序

1. 不变式核心通常是弱化后的后置条件。
2. 设计带守卫的指令，以保持不变式并减小界函数。
3. 满足以下条件时，情况覆盖充分：Invariant ∧ ¬(B₁ ∨ B₂ ∨ ... ∨ Bₙ) ⟹ Post。

---

工作流摘要

编写任何函数时，都应遵循以下流程：

1. 明确规范： 写出前置条件和后置条件。确定输入和输出类型。
2. 分析后置条件： 判断解决方案是否需要赋值、条件判断、递归或迭代。
3. 选择策略：
   • 后置条件简单且由等式构成 → 直接赋值／组合。
   • 存在析取 → 条件判断／分支。
   • 存在归纳结构 → 递归或迭代。
4. 对于递归解决方案：
   • 确定各个情形（直接情形 + 递归情形）。
   • 定义有界函数。
   • 验证每种情形。
   • 如有需要，考虑使用浸入技术来提高效率或实现尾递归。
5. 对于迭代解决方案：
   • 推导不变式（弱化后的后置条件）。
   • 定义有界函数。
   • 设计循环体，使其保持不变式并减小界限。
   • 设置初始化代码和循环后代码。
6. 验证： 确保满足所有证明义务，或推导出能从构造上保证这些义务成立的代码。

---

应用此技能

生成或审查任何语言的代码时：

• 始终从前置条件和后置条件的角度思考，即使语言本身不强制要求。将它们记录为注释、断言、类型约束或契约。
• 使用语言中可用的断言／契约（assert、require、ensure、契约式设计库、基于属性的测试）来编码前置／后置条件。
• 设计递归函数时，明确指出有界函数并验证终止性。
• 设计循环时，明确写出不变式和有界函数。
• 优先从规范推导代码，而不是先编写代码再进行测试。
• 递归解决方案不是尾递归时，考虑使用浸入技术进行转换。
• 对数据结构使用代数推理：通过方程定义操作，并使用结构归纳法进行推理。
• 在语言支持的情况下，将有界函数编码为递减度量（例如 Dafny 的 decreases、Coq 的结构递归或手动断言）。

---

将形式化规范与测试关联起来

形式化规范（前置条件和后置条件）与测试用不同语言表达了同一个想法：前者使用逻辑，后者使用可执行代码。根据规范而非实现推导测试，便能形成闭环：使代码正确的同一套推理，也能保证测试正确。

1. 规范 → 测试

形式化规范中的每个元素都对应一项具体测试：

形式化元素	对应的测试
前置条件不满足	非正常路径测试 — 断言函数会报错
后置条件等式 r = E	相等断言（toBe、expectEqual、assert { condition = ... }）
后置条件析取 A ∨ B	每个分支各一个测试
基础构造子（[]、empty、0）	基础情形测试 — 验证量词的中性元素
归纳构造子（e:l、plant(...)）	使用最小非平凡值进行测试

示例 — sum(list)

function sum(list) returns result
  {Pre:  list is a list of numbers}
  {Post: result = Σ(a: a ∈ list: a)}

Σ 的中性元素是 0，因此基础情形为 sum([]) = 0。归纳构造子 e:l 产生最小测试 sum([5]) = 5，一般情形为 sum([1, 2, 3]) = 6。

TypeScript（Jest / Vitest）

// sum.test.ts
import { sum } from "./sum";

it("returns 0 for empty list — neutral element of Σ", () => {
  expect(sum([])).toBe(0);
});

it("returns the element itself for a singleton — minimal inductive case", () => {
  expect(sum([5])).toBe(5);
});

it("returns the total for a general list", () => {
  expect(sum([1, 2, 3])).toBe(6);
});

it("rejects non-numbers — precondition violation", () => {
  expect(() => sum(["a"] as any)).toThrow();
});

Go（testing）

// sum_test.go
func TestSumEmptyList(t *testing.T) {
    // Base case: neutral element of Σ is 0
    if got := Sum([]int{}); got != 0 {
        t.Errorf("Sum([]) = %d, want 0", got)
    }
}

func TestSumSingleton(t *testing.T) {
    // Minimal inductive case: one recursive step falling into base case
    if got := Sum([]int{5}); got != 5 {
        t.Errorf("Sum([5]) = %d, want 5", got)
    }
}

func TestSumGeneralList(t *testing.T) {
    if got := Sum([]int{1, 2, 3}); got != 6 {
        t.Errorf("Sum([1,2,3]) = %d, want 6", got)
    }
}

2. 测试递归情形

每个递归函数都具有以下结构：

function f(x):
  if d(x)  → h(x)           -- direct case
  ¬d(x)    → c(x, f(s(x)))  -- recursive case

此结构直接决定了测试套件：

• 直接情形（d(x) 为真）：测试基本情形。预期值是后置条件所表达的量词的中性元素。
• 最小递归情形（¬d(x) 且 s(x) 落入直接情形）：使用能恰好触发一次递归调用的最小输入进行测试。
• 一般情形：使用能触发多次递归调用的输入进行测试。
• 界限函数 t(x)：当终止性不明显时，使用调用计数器或 spy，确认递归调用次数不超过 t(x_initial)。

示例 — length(list)

function length(list) returns n
  {Pre:  list is a list}
  {Post: n = N(a: a ∈ list: true)}
  if list = []  → n := 0                      -- d(x): list is empty
  list ≠ []     → n := 1 + length(tail(list)) -- recursive case

界限函数：t(list) = length(list)（输入结构的大小）。

TypeScript（Jest / Vitest）

// length.test.ts
import { length } from "./length";

it("returns 0 for empty list — direct case, neutral of N", () => {
  expect(length([])).toBe(0);
});

it("returns 1 for singleton — one recursive call into base", () => {
  expect(length([7])).toBe(1);
});

it("returns correct length for general list", () => {
  expect(length([1, 2, 3])).toBe(3);
});

Go（testing）

// length_test.go
func TestLengthEmpty(t *testing.T) {
    if got := Length([]int{}); got != 0 {
        t.Errorf("Length([]) = %d, want 0", got)
    }
}

func TestLengthSingleton(t *testing.T) {
    if got := Length([]int{7}); got != 1 {
        t.Errorf("Length([7]) = %d, want 1", got)
    }
}

func TestLengthGeneral(t *testing.T) {
    if got := Length([]int{1, 2, 3}); got != 3 {
        t.Errorf("Length([1,2,3]) = %d, want 3", got)
    }
}

Zig（std.testing + comptime 表）

在 Zig 中，对多个情形进行测试的惯用模式是使用 inline for 遍历 comptime 数组——零开销的参数化测试，无需外部库：

const std = @import("std");
const length = @import("length").length;

test "length — direct case, recursive case, general" {
    const cases = comptime [_]struct {
        input: []const i32,
        expected: usize,
    }{
        .{ .input = &[_]i32{},        .expected = 0 }, // direct case: d(x)
        .{ .input = &[_]i32{7},       .expected = 1 }, // minimal recursive case
        .{ .input = &[_]i32{ 1, 2, 3 }, .expected = 3 }, // general case
    };

    inline for (cases) |c| {
        try std.testing.expectEqual(c.expected, length(c.input));
    }
}

3. 针对全称后置条件的基于属性测试

当后置条件包含全称量词（∀）时，手动测试只能验证无限真理中的有限个情形。基于属性测试（PBT）会生成随机输入，逐一检查属性，并在失败时将反例缩减为最小失败情形。

**规则：**如果后置条件的形式为 ∀x ∈ domain: P(x)，就编写属性测试，而不仅仅是示例测试。

示例 — reverse 的代数属性

{Post₁: ∀l: length(reverse(l)) = length(l)}   -- reverse preserves length
{Post₂: ∀l: reverse(reverse(l)) = l}           -- reverse is an involution

TypeScript — fast-check

// reverse.property.test.ts
import * as fc from "fast-check";
import { reverse } from "./reverse";

test("Post₁: reverse preserves length — ∀l", () => {
  fc.assert(
    fc.property(fc.array(fc.integer()), (l) => {
      return reverse(l).length === l.length;
    })
  );
});

test("Post₂: reverse is an involution — ∀l", () => {
  fc.assert(
    fc.property(fc.array(fc.integer()), (l) => {
      const rr = reverse(reverse(l));
      return rr.length === l.length && l.every((v, i) => v === rr[i]);
    })
  );
});

Go — rapid

// reverse_property_test.go
import (
    "testing"
    "pgregory.net/rapid"
)

func TestReversePreservesLength(t *testing.T) {
    // Post₁: ∀l: length(reverse(l)) = length(l)
    rapid.Check(t, func(t *rapid.T) {
        l := rapid.SliceOf(rapid.Int()).Draw(t, "l")
        if len(Reverse(l)) != len(l) {
            t.Fatalf("length(Reverse(%v)) ≠ length(%v)", l, l)
        }
    })
}

func TestReverseIsInvolution(t *testing.T) {
    // Post₂: ∀l: reverse(reverse(l)) = l
    rapid.Check(t, func(t *rapid.T) {
        l := rapid.SliceOf(rapid.Int()).Draw(t, "l")
        got := Reverse(Reverse(l))
        if len(got) != len(l) {
            t.Fatalf("len(Reverse(Reverse(%v))) = %d, want %d", l, len(got), len(l))
        }
        for i := range l {
            if got[i] != l[i] {
                t.Fatalf("Reverse(Reverse(%v)) = %v, want %v", l, got, l)
            }
        }
    })
}

Zig — comptime 表 + 内置模糊测试器

Zig 没有惯用的 PBT 库。可使用以下两种互补方法：

1. 使用 inline for 遍历 comptime 数组，测试根据规范得出的代表性情形（基本情形、最小归纳情形、边界值）。
2. 使用 zig test --fuzz 测试不会崩溃或触发 panic 的不变量——内置模糊测试器会提供任意字节，并捕获 panic、越界访问和未定义行为。

const std = @import("std");
const reverse = @import("reverse").reverse;

// Post₁ + Post₂: representative cases covering base and inductive constructors
test "reverse — spec-derived cases" {
    const allocator = std.testing.allocator;
    const cases = comptime [_]struct {
        input: []const i32,
        expected: []const i32,
    }{
        .{ .input = &[_]i32{},        .expected = &[_]i32{} },
        .{ .input = &[_]i32{1},       .expected = &[_]i32{1} },
        .{ .input = &[_]i32{ 1, 2, 3 }, .expected = &[_]i32{ 3, 2, 1 } },
    };

    inline for (cases) |c| {
        const result = try reverse(allocator, c.input);
        defer allocator.free(result);
        try std.testing.expectEqual(c.expected.len, result.len);
        try std.testing.expectEqualSlices(i32, c.expected, result);
    }
}

// Post₁ no-panic invariant: reverse must not crash on any input
test "reverse — fuzz no-panic" {
    const input = std.testing.fuzzInput(.{});
    const allocator = std.testing.allocator;
    const n = input.len / @sizeOf(i32);

    // Decode fuzz bytes into i32 values without assuming alignment.
    var buf = std.ArrayList(i32).init(allocator);
    defer buf.deinit();
    try buf.ensureTotalCapacity(n);

    var i: usize = 0;
    while (i < n) : (i += 1) {
        const base = i * @sizeOf(i32);
        const chunk = input[base .. base + @sizeOf(i32)];
        const value = std.mem.bytesToValue(i32, chunk);
        buf.appendAssumeCapacity(value);
    }

    const data: []const i32 = buf.items;
    const result = reverse(allocator, data) catch return;
    defer allocator.free(result);
    try std.testing.expectEqual(data.len, result.len);
}
// Run with: zig test reverse_test.zig --fuzz

Terraform — 原生 terraform test（.tftest.hcl）

Terraform 不支持 PBT。全称后置条件（∀）通过 assert 块中的 alltrue([for ... : ...]) 表达。边界情形和前置条件违规各自使用单独的 run 块——.tftest.hcl 中没有循环。

# tests/subnets_unit_test.tftest.hcl

# Post: ∀subnet ∈ aws_subnet.private: subnet.cidr_block ∈ "10.0.0.0/8"
run "all_private_subnets_in_range" {
  command = plan

  assert {
    condition = alltrue([
      for s in aws_subnet.private : can(regex("^10\\.0\\.", s.cidr_block))
    ])
    error_message = "All private subnets must be in the 10.0.x.x range."
  }
}

# Pre violated: cidr_block outside allowed range must be rejected
run "invalid_cidr_rejected" {
  command = plan

  variables {
    cidr_block = "192.168.1.0/24"
  }

  expect_failures = [var.cidr_block]
}

# Boundary: minimum allowed subnet count
run "minimum_subnet_count" {
  command = plan
  variables { subnet_count = 1 }

  assert {
    condition     = length(aws_subnet.private) == 1
    error_message = "Expected exactly 1 subnet."
  }
}

# Boundary: zero subnets must be rejected by variable validation
run "zero_subnets_rejected" {
  command = plan
  variables { subnet_count = 0 }

  expect_failures = [var.subnet_count]
}

4. 组合工作流

形式化推导和 TDD 并非二选一，而是同一流程的两个层次。规范是事实来源；代码和测试都由规范独立推导而来。

1. Specify   Write Pre and Post formally.
             Identify the quantifier structure (Σ, ∀, N, ...) and its neutral element.
             Identify constructors of the input type (base + inductive).

2. Red       Translate Pre/Post into tests — all must fail (code does not exist yet):
             · Pre violated              → unhappy-path test / expect_failures
             · Base constructor          → test of the quantifier's neutral element
             · Minimal inductive case    → test with one recursive step into base
             · Postcondition with ∀      → property test (fast-check / rapid)
                                           or alltrue([for...]) in Terraform
             · Each postcondition branch → one test per disjunct

3. Derive    Construct the code from the postcondition analysis (not from the tests).
             Choose the strategy that matches the postcondition structure:
             equalities → assignment, disjunctions → conditional, inductive → recursion/loop.

4. Green     The tests pass on the first run — by construction, not by adjustment.
             If a test fails, the derivation has a gap: re-examine the proof obligation.

5. Refactor  Improve structure, names, efficiency. The tests stay green.
             The formal invariant guarantees that refactoring preserves correctness.
             Immersion (tail-recursion transformation) is a safe refactoring step
             because the postcondition is unchanged.

**关键见解：**当代码和测试都从同一规范推导而来时，红—绿—重构循环便简化为 编写规范 → 推导 → 验证。针对规范（而非实现）编写的测试，不会因为错误代码恰好与测试相符而意外通过。测试会因为正确的原因失败，也会因为正确的原因通过。