RFC-027：编译期谓词与统一静态验证

参考:
RFC-009: 所有权模型
RFC-010: 统一类型语法 - name: type = value 模型
RFC-011: 泛型系统设计
RFC-024：基于 spawn 块的并发模型
取代：RFC-022: 霍尔逻辑静态验证支持（规约注释与规约类型） — 已废弃

摘要

本文提出为 YaoXiang 引入编译期谓词作为一等公民，将所有编译期静态验证统一为一条证明管道。编译期谓词不是外挂的规约注释——它就是函数。一个返回 Type 的函数，可在类型位置使用，编译器在编译期调用它并检查返回值。类型即命题，编译期求值即证明。

核心论点：类型检查在编译期唯一的工作就是构造和验证证明项。类型等式、令牌冲突、依赖类型归约、编译期谓词求值、霍尔逻辑蕴含——全部是编译期证明管道中的不同类型检查，共享同一条管道。SMT 求解器是类型检查器的加速模块，不是独立的信任边界。当编译器返回 Unproven 时，程序员写一个 YaoXiang 函数作为证明——类型检查器以与验证任何函数返回类型完全相同的方式验证它。一切都是 YaoXiang 代码，一切由类型检查器验证。

动机

为什么废弃 RFC-022？

RFC-022 将规约设计为 //! 注释形式：

yaoxiang

max: (T: Ord) -> ((arr: Array(T, n)) -> T) = {
    //! requires: NonEmpty(n) = n > 0          ← 这是独立于类型的注释
    //! ensures: ExistsMax(result, arr[0..n])   ← 这是独立于类型的注释
}

这犯了 Curry-Howard 同构的根本性错误：将规约和类型分裂为两层。注释不是类型。注释不参与类型检查。注释是"外部工具"的心智模型。

白皮书说得很清楚：

"没有 //! 注释。没有独立的规约语言。一切都在类型系统内。"

当前的问题

RFC-022 的 //! 注释是独立于类型系统的外挂语法
规约类型和普通类型是两套体系，造成概念冗余
Debug Build 验证 / Release Build 忽略的分裂模式破坏了统一性
SMT 求解器在传统认知中被定位为外部工具——YaoXiang 将其作为类型检查器的加速模块内置
类型检查、借用验证、编译期谓词检查、宏展开各自走不同的路径

正确的心智模型

类型检查可以抽象为一个函数：

verify : Program → Proved | Disproved(Model) | Unproven

所有编译期检查——简单类型匹配、借用冲突检测、编译期谓词验证——都是这个函数的子任务。它们共享同一条证明管道，区别仅在于证明项复杂度和构造策略。

当编译器返回 Unproven 时，程序员提供一个证明函数——该函数的返回类型等于待证命题。类型检查器验证它。这和平常的类型检查是同一个操作。

提案

1. `{}` 是证明空间：类型即断言，验证即类型检查

YaoXiang 的 {} 是编译期证明空间。里面的一切都是断言，编译器保证每一项为 True——要么自动证明，要么由程序员提供证明函数。

Point: Type = { x: Float, y: Float }
#               ^^^^^^^^^^^^^^^^^^^^^  编译器保证 x 是 Float，y 是 Float

List: (T: Type) -> Type = { data: Array(T) }
#                           ^^^^^^^^^^^^^^^  编译器保证 data 是 Array(T)

泛型是编译期谓词的特例。

yaoxiang

Positive: (x: Int) -> Type = { x > 0 }
#          ^^^^^^              ^^^^^^
#          参数在签名处          {} 内只有断言
#          编译器在编译期调用时验证 x > 0

List: (T: Type) -> Type = { data: Array(T) }
#      ^^^^^^^^              ^^^^^^^^^^^^^^^
#      参数在签名处           编译器验证 type_of(T) == Type，type_of(data) == Array(T)

同一个模式：name: (params) -> Type = { 断言 }。编译器不区分"类型断言"和"值断言"——都是证明管道中的求值目标。

循环不变式不需要单独写。变量上的类型标注就是 Floyd-Hoare 不变式。

yaoxiang

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0   # 标注引用 i——告诉编译器 s 的类型依赖 i
    mut i: UpTo(arr.len) = 0     # 初始化时 i=0，验证：0 == sum(arr[0..0]) → True
    while i < arr.len {
        s += arr[i]  # 编译器验证：s_new == sum(arr[0..i+1])
        i += 1       # i 变更→触发 s 依赖重验证：s 满足 SumUpTo(arr, i_new)
    }
    return s  # s: SumUpTo(arr, arr.len) = sum(arr[0..arr.len])
}

编译器对循环体生成一次验证条件——归纳假设（类型标注）→ 赋值操作 → 新值是否满足类型标注。证明管道验证归纳步成立后，所有迭代自动覆盖。不需要 : decreases，不需要 : Invariant，不需要归纳证明——编译器把归纳分解为每个赋值的局部 VC。

2. 前置/后置条件：参数类型和返回类型上的编译期谓词

放弃 RFC-022 的 //! requires///! ensures。编译期谓词作为参数或返回的类型标注。

参数侧是函数调用。 编译期谓词是返回 Type 的函数，参数侧的使用方式就是调用它——和 factorial(5) 一样。返回值侧引入了一个新概念：返回值形参。

yaoxiang

# 前置条件：参数类型中显式调用编译期谓词
Positive: (x: Int) -> Type = { x > 0 }

divide: (a: Int, b: Positive(b)) -> Int = a / b
#                       ^^^^^^^^^^  b 是当前形参名，传给 Positive 做参数
#                       编译器在调用点提取实参值，代入 b，验证 Positive(实参)
#                       例：divide(10, 2) → 验证 Positive(2) = { 2 > 0 } → True
#                       例：divide(10, 0) → 验证 Positive(0) = { 0 > 0 } → False → 编译错误

# 后置条件：返回值形参 + 编译期谓词
IsMax: (T: Ord, arr: Array(T), result: T) -> Type = {
    forall j in 0..arr.len: result >= arr[j]
}

NonEmpty: (arr: Array(T)) -> Type = { arr.len > 0 }

max: (T: Ord) -> ((arr: NonEmpty(arr))) -> (result: IsMax(T, arr, result)) = {
#                                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
#                                            result 是返回值形参，值由 return 提供
#                                            编译器在 return 点代入返回值，验证后置条件
    candidate = arr[0]
    for i in 1..arr.len {
        if arr[i] > candidate { candidate = arr[i] }
    }
    return candidate
}

关键规则：

参数侧：b: Positive(b) —— b 是当前形参名，传给 Positive 做参数。函数调用语法，零隐式。
返回侧：-> (result: IsMax(T, arr, result)) —— result 是返回值形参，值由 return 语句提供。result 仅存在于类型签名中、仅被谓词引用，不进入函数体作用域、不出现在调用方。
返回值形参可选：无后置条件时不写，签名和普通函数完全一致（-> Int）。
统一性：参数和返回值形参是同一个概念——形参名: 谓词调用(形参名)，区别仅在于值由调用方提供还是由 return 提供。

3. 路径条件传播：运行时值的编译期验证

编译期谓词在绑定位置使用时，参数由程序员显式传入。当运行时值进入精化类型参数时，编译器通过路径条件收集和 SMT 蕴含判断完成验证——无需程序员显式传递证明。

3.1 显式函数调用

编译期谓词在绑定位置使用时，参数由程序员显式传入——就是函数调用，零隐式。

Positive: (x: Int) -> Type = { x > 0 } 是一个编译期谓词构造器。当它出现在绑定位置（参数声明、变量声明、返回类型）时，程序员显式传入已绑定的变量名：

yaoxiang

b: Positive(b)
// b 已被声明为当前形参，Positive(b) 是函数调用
// 正格化后：b: { b > 0 }

不需要编译器隐式填入参数——b: Positive(b) 和 f(5) 一样，就是函数调用。b 作为参数名被绑定，其类型标注 Positive(b) 引用了 b 自身——这是依赖类型的标准模式，不是隐式展开规则。

与 RFC-010 self 的统一：RFC-010 确立 self 不是关键字，只是参数名的约定俗成（"写成 p、this、x 效果完全一样"）。b: Positive(b) 共享同一个机制——参数名在类型标注中可被引用。self 出现在 self: Point 的位置，b 出现在 b: Positive(b) 的位置，两者的类型标注都引用了参数自身。区别仅在于类型标注的复杂度，机制完全一样——名字绑定后，类型可以依赖这个名字。

返回类型同样使用显式函数调用：

yaoxiang

Sorted: (arr: Array(T)) -> Type = { forall i in 0..arr.len-1: arr[i] <= arr[i+1] }

sort: (arr: Array(T)) -> (result: Sorted(result)) = { ... }
//                        ^^^^^^^^^^^^^^^^^^^^^^^
//                        result 是返回值形参，Sorted(result) 是函数调用
//                        编译器在 return 点将返回值代入 result，验证 Sorted(返回值)

同样适用于局部变量声明：

yaoxiang

let x: Positive(x) = 5
// x 绑定为 5，Positive(5) → { 5 > 0 } → True → 通过

// let y: Positive(y) = 0
// y 绑定为 0，Positive(0) → { 0 > 0 } → False → 编译错误

3.2 路径条件收集

当运行时值出现在条件分支中时，编译器自动收集路径条件，形成当前作用域的假设集合。这些假设作为编译期 Bool 求值的背景知识参与验证。

yaoxiang

if y > 0 {
    // 编译器在此分支内自动获得假设：{ y > 0 }
    let result = divide(x, y)
    // 验证条件：(y > 0) ⇒ (y > 0)
    // 证明管道判蕴含成立 → Proved
} else {
    // 此分支假设：{ !(y > 0) }
    // 如果要调用 divide(x, y)，验证条件为 !(y > 0) ⇒ y > 0
    // 证明管道判不蕴含 → Disproved
}

这不是编译器写死特殊模式——这是编译期证明管道的自然行为。每次类型检查调用点向管道发送：

{背景假设} ⇒ {验证目标}

证明管道判断蕴含性。Proved → 通过，Disproved → 编译错误 + 反例，Unproven → 编译错误 + 未解命题。背景假设来自当前程序点的路径条件。

3.3 假设栈

编译器在分析控制流时，为每个基本块维护一个假设集合：

if-guard：if y > 0 → true 分支压入 y > 0，false 分支压入 !(y > 0)（如果使用了 else）
match 模式：if let Some(v) = opt → 分支内压入 opt == Some(v)
逻辑连接：if x > 0 && y < 10 → 分支内压入 x > 0 和 y < 10
函数前置条件：调用 divide(a, b) 时，b 必须满足 Positive 的证据要么来自当前假设，要么来自实参自身的精化类型标注（b 已被标注为 Positive 则其类型携带 b > 0）
赋值：let z = y 时，y 上已有的精化条件传递到 z

所有假设进入编译期证明管道。当进入 SMT 加速路径时，翻译为 SMT-LIB 背景断言。

3.4 无静态证据则编译错误

如果程序员直接写：

yaoxiang

divide_user_input: (x: Int, y: Int) -> Int = divide(x, y)

当前程序点没有 y > 0 的假设，实参 y 自身也没有 Positive 类型标注。验证条件为：

{} ⇒ { y > 0 }

管道返回 Disproved（不蕴含）→ 编译错误：

无法证明参数 b 在 divide 调用中满足 Positive。 y 来自函数输入，无已证明的界。考虑用 if 分支守卫调用：if y > 0 { divide(x, y) }。

YaoXiang 不接受运行时值直接进入精化类型参数而不提供静态证据。这不是限制——这是硬安全哲学的核心。凡编译器无法静态证明的代码，不得通过编译。

3.5 与统一管道的关系

路径条件传播不是额外的机制。它是编译期证明管道在控制流分析上的直接延伸：

阶段	职责
路径条件收集	编译器控制流分析阶段，为每个基本块标注假设集
验证条件生成	遇到需验证的类型约束时，合并路径条件 + 实参类型信息
证明管道求值	编译器内核 → SMT 加速 → 得出 Proved / Disproved / Unproven
结果	`Proved` → 通过；`Disproved` → 编译错误 + 反例；`Unproven` → 编译错误 + 未解命题（程序员可提供证明函数）

没有新部件。没有特殊规则。路径条件就是证明管道的背景知识——和类型等式、借用约束共享同一条管道、同一套预算系统。

4. 编译期证明管道

所有编译期检查共享同一条管道。管道的核心操作是类型检查——检查一个证明项的类型是否等于待证明的命题。一切皆类型检查。

编译期遇到 Bool 表达式需要求值（即：需要构造一个证明项）
        │
        ├── 类型等式（T1 == T2）
        │   → 编译器直接判定（结构等价）
        │
        ├── 令牌冲突条件（!conflicting(tokens)）
        │   → 流敏感活性分析（Dup/Linear 属性追踪）
        │
        ├── 依赖类型归约（n + m 化简）
        │   → 编译期项重写系统（βδι-规约）
        │
        ├── 编译期谓词（x > 0, forall...）
        │   → 编译器自身 + SMT 加速模块
        │
        └── 霍尔逻辑蕴含式（P ⇒ Q）
            → 编译器 + SMT 加速模块
                    │
                    ▼
             ┌──────────┐
             │ Proved   │  → 编译通过
             │ Disproved│  → 编译错误 + 反例
             │ Unproven │  → 编译错误 + 未解命题
             └────┬─────┘
                  │
                  ▼
         程序员写证明函数（YaoXiang 代码）
                  │
                  ▼
         类型检查器验证 ──→ Proved ──→ 编译通过
                  │
                  ▼
            验证失败 → 编译错误："证明不成立"

4.1 证明结果：三值代数

编译期求值返回三种结果——这是停机问题的必然结论，也是证明论的自然分划：

eval_compile_time : BoolExpr → Proved | Disproved(Model) | Unproven

Proved → 停机，证明项已构造，类型检查通过。编译继续。
Disproved(M) → 停机，存在反例 M。编译错误 + 反例 + 源码位置。
Unproven → 在给定资源上限内未构造出证明。编译错误 + 未解命题 + 预算消耗报告。

Unproven ≠ False。 编译器说"我证明不了"不等价于命题为假——只是超出了当前自动证明的能力。这是诚实，不是缺陷。

预算硬限制是停机问题的工程解。不给 knob——给了就是在问用户"你觉得你的程序会不会停机"，用户不知道，编译器也不知道。

4.2 Unproven 之后：程序员写证明

当编译器返回 Unproven 时，程序员可以写一个证明函数——就是一个 YaoXiang 函数，其返回类型等于待证明的命题。类型检查器验证这个函数——和它验证 add(a, b): Int 是同一个机制。

命题  = 类型
证明  = 程序（该类型的一个值）
验证  = 类型检查（唯一的信任根）

SMT 求解器不是独立的信任边界——它是类型检查器的加速模块。SMT 帮忙找证明，但验证证明的始终是类型检查器。SMT 返回 unsat 时，编译器将其结果重构为类型检查器可验证的证明项。如果重构失败（SMT 的推理步骤超出编译器内核的推理规则），则回退到 Unproven——程序员可以手动写证明函数。

yaoxiang

# 命题：编译器无法自动证明的精化属性
FirstIsMin: (T: Ord, arr: Sorted(T)) -> Type = {
    forall i in 0..arr.len: arr[0] <= arr[i]
}

# 证明：程序员写一个函数，返回类型就是上面的命题
# 类型检查器验证这个函数——和验证 add(a,b): Int 完全一致
first_is_min: (T: Ord, arr: Sorted(T)) -> FirstIsMin(T, arr) = {
    # 编译器在此验证：函数体的类型 = FirstIsMin(T, arr)
    ...
}

不需要 AI，不需要导出到 Coq，不需要新概念。编译期无法自动证明的属性 → 程序员用 YaoXiang 代码写证明 → 类型检查器验证。 整个过程是平滑的梯度——编译器替你做了简单的证明，把脑子留给难的。

4.3 管道内的分层依赖

以上求值器共享同一接口但存在求值顺序。类型等式是所有后续分析的先决条件；所有权/令牌检查依赖类型信息；精化谓词验证依赖前两层的结果。编译器按层求值，底层失败的表达式不进入上层——避免在类型错误的程序上浪费求解预算。

求值顺序（同一管道，分层调度）
├── 第 0 层：类型等式（T1 == T2）
│   └── 结构合一 → 失败则后续无意义，直接返回 Disproved
├── 第 1 层：所有权/令牌冲突
│   └── 流敏感活性分析 → 失败则内存安全不成立，直接返回 Disproved
└── 第 2 层：精化谓词/霍尔蕴含
    └── 编译器自身 → SMT 加速 → 得出 Proved / Disproved / Unproven

每一层仍返回 Proved/Disproved/Unproven，共享同一接口和同一预算系统。

5. 三层函数统一

层级	运行时机	输入	输出	示例
值级函数	运行时	值	值	`add: (a: Int, b: Int) -> Int = a + b`
类型构造器	编译期	类型/值	Type	`List: (T: Type) -> Type = { data: Array(T) }`
编译期谓词	编译期	值	Type	`Positive: (x: Int) -> Type = { x > 0 }`

全部使用相同的 name: type = value 语法。编译期谓词和类型构造器走同一条编译期证明管道——{} 是证明空间。

6. 循环：Floyd-Hoare 验证条件生成

循环不需要单独的 : Invariant(...) 或 : decreases(...) 标注。变量上的编译期谓词类型标注定义了 Floyd-Hoare 风格的断言——编译器从类型标注生成验证条件，证明管道检查每个赋值是否保持类型。

核心机制：每个赋值操作对应一个 Hoare 三元组 {P} x := e {Q}，验证条件是 P ⇒ Q[e/x]。编译器对循环体生成一次验证条件——证明管道验证归纳步成立后，所有迭代自动覆盖。

yaoxiang

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0   # 标注引用 i；初始化时 i=0，验证：0 == sum(arr[0..0]) → True
    mut i: UpTo(arr.len) = 0     # 验证：0 <= 0 <= arr.len → True
    while i < arr.len {
        # 编译器对循环体生成一次 VC。前提：s 满足 SumUpTo(arr, i)，i 满足 UpTo(arr.len)。
        #
        # s += arr[i]：
        #   验证义务：s_new 满足 SumUpTo(arr, i)（当前 i 不变）
        #   代入 s_new = s_old + arr[i]：
        #     需要 s_old + arr[i] == sum(arr[0..i+1])
        #     从归纳假设 s_old == sum(arr[0..i])，两边加 arr[i]：
        #     sum(arr[0..i]) + arr[i] == sum(arr[0..i+1])
        #   编译器 + SMT：线性算术，毫秒级 → Proved
        #
        # i += 1：
        #   i 变更 → 依赖图中 s 的类型标注引用了 i → 触发重验证
        #   新的验证目标：s 满足 SumUpTo(arr, i_new)
        #   即 s == sum(arr[0..i_new])，由上一步保证 → Proved
        s += arr[i]
        i += 1
    }
    return s  # 此时 s: SumUpTo(arr, arr.len)，即 s == sum(arr[0..arr.len])
}

循环不变式就是变量上的类型标注——程序员写类型，编译器检查归纳步。编译器不需要"发现"不变式，也不需要"自动做归纳"——它把归纳证明分解为每个赋值操作的局部验证条件，交给证明管道分而治之。

6.1 依赖追踪：可变变量上的依赖类型

上述机制的前提是：编译器知道 s 的类型标注 SumUpTo(arr, i) 引用了 i——当 i 变更时，s 的类型约束也随之变化。这需要编译器维护变量间的类型依赖图。

数据结构：

TypeDepGraph: Map<VarName, Set<VarName>>
# 键是被依赖的变量，值是类型标注中引用了该变量的变量集合
# 例：{ i: {s}, j: {s, t}, ... }

构建：类型检查器在处理 mut v: Pred(... x ...) = init 时，解析 Pred(...) 参数中的自由变量引用。如果参数中引用了当前作用域内的其他可变变量 x，则在依赖图中记录 x → v。

触发：当被依赖的变量 x 被赋值时，编译器：

查找依赖图中所有依赖 x 的变量 {v₁, v₂, ...}
对每个 v，生成验证条件：v 的当前值是否满足更新后的类型 Pred(... x_new ...)
将 VC 送入证明管道

赋值顺序敏感：依赖追踪自然强制执行正确的赋值顺序。以 SumUpTo(arr, i) 为例：

yaoxiang

# 正确顺序
s += arr[i]   # s_new 满足 SumUpTo(arr, i+1)
i += 1        # i 变更 → 重验证 s 满足 SumUpTo(arr, i_new) → True

# 错误顺序——编译器拒绝
i += 1        # i 变更 → 重验证 s 满足 SumUpTo(arr, i_new)
              # s 尚未更新，s_old == sum(arr[0..i_old]) ≠ sum(arr[0..i_new])
              # → 编译错误：变量 s 不满足类型 SumUpTo(arr, i_new)
s += arr[i]   # 不可达

组合依赖：一个变量可以依赖多个变量。类型标注 { v: Int; v == x + y } 同时依赖 x 和 y——任一变更都触发重验证。

与证明管道的关系：依赖追踪是 VC 生成的触发器，不是独立的验证机制。它回答"什么时候需要生成 VC"——证明管道回答"VC 是否成立"。

7. 终止检查

编译期全自动。编译器能证明的循环通过，不能证明的直接报编译错误——程序员必须让编译器能自动分析循环的终止性。不给半自动标注留口子。

6.1 设计原则

编译器从两处自动提取终止证明所需的信息：

变量类型标注：精化类型中的边界约束（如 UpTo(n) 给出上界 n 和下界 0）
循环体操作：每次迭代对变量施加的操作

编译器按优先级尝试四种度量合成策略，找到一个即停止。

6.2 策略 1：线性秩函数自动合成

当变量有线性界标注时，编译器枚举候选线性度量并 SMT 验证。

输入：
  变量 v₁: UpTo(u₁), v₂: UpTo(u₂), ...（有上下界的变量）
  循环条件 cond
  循环体中的赋值集合

算法：
  1. 从类型标注提取每个变量的界：[low_i, high_i]
  2. 枚举候选度量：v_i, u_i - v_i, v_i - v_j, 等线性组合
  3. 对每个候选度量 m：
     - SMT 验证 m ≥ 0（从类型界推导）
     - 对循环体的每条执行路径，SMT 验证 m' < m（严格递减）
  4. 找到符合条件的线性组合 → 终止得证

覆盖范围：任意变量被赋值为线性表达式（v = a·v + b）且有界类型标注的循环。包括 i += const、i -= const、以及二分查找式的区间收缩：

yaoxiang

# 二分查找：low = mid + 1 或 high = mid
# 度量 high - low 在两条路径上都严格递减
binary_search: (arr: Sorted(Int, arr), key: Int) -> Option(Int) = {
    mut low: UpTo(arr.len) = 0
    mut high: UpTo(arr.len) = arr.len
    while low < high {
        let mid = (low + high) / 2
        if arr.data[mid] < key { low = mid + 1 }
        else if arr.data[mid] > key { high = mid }
        else { return Some(mid) }
    }
    return None
}

6.3 策略 2：谓词违反计数——从目标类型自动提取度量【实验性策略】

⚠️ 当前状态：实验性策略，阶段 3 实现时根据实际可行性决定是否包含。 此策略对相邻交换操作（冒泡排序、插入排序）有效，对非相邻操作（快速排序 partition、堆排序 sift-down）无法自动证明。覆盖边界见下表。如阶段 3 验证不可行，此策略将被移除或降级为未来工作。

核心洞察：用户写的规约是编译器推理的素材。 编译器不需要内置"什么是排序"——它读 Sorted 的定义，从定义中自动提取度量。

输入：
  目标类型：Sorted(arr) = { forall i in 0..arr.len-1: arr[i] <= arr[i+1] }
  循环体操作：相邻元素交换

算法：
  1. 解析谓词定义：forall i in range: cond(i, arr)
  2. 自动生成度量：violation_count = |{ i | ¬cond(i, arr) }|
  3. 分析操作对度量的影响：
     - 相邻交换 arr[j], arr[j+1] = arr[j+1], arr[j]
     - 只影响索引 j-1, j, j+1 三对
     - 如果 arr[j] > arr[j+1]（违反谓词），交换后这对满足谓词
     - violation_count 至少减 1
  4. 上界：n·(n-1)/2（最大相邻逆序数），下界：0
  → 终止得证

当前覆盖范围：

算法	操作模式	策略 2 可证明？	原因
冒泡排序	相邻交换	✅	violation_count 每次交换严格递减
插入排序	相邻移动	✅	每次移位消除一个违反对
选择排序	非相邻交换	❌	单次交换可能增加 violation_count
快速排序	partition 分区	❌	非相邻交换，不保证单调递减
堆排序	sift-down	❌	树形操作，violation_count 非单调

互补策略：对于快速排序，low < high 区间收缩可由策略 1（线性秩函数）覆盖——外层的 partition 递归，每次区间减半。策略 1 和策略 2 互补覆盖，多数实际算法的终止性可由两者之一证明。但策略 2 的通用化（非相邻操作、树形操作）仍是开放问题。

yaoxiang

sort: (arr: Array(Int)) -> (result: Sorted(result)) = {
    mut i: UpTo(arr.len) = 0
    while i < arr.len - 1 {
        mut j: UpTo(arr.len - i - 1) = 0
        while j < arr.len - i - 1 {
            if arr.data[j] > arr.data[j+1] {
                arr.data[j], arr.data[j+1] = arr.data[j+1], arr.data[j]
            }
            j += 1
        }
        i += 1
    }
    return arr
}

6.4 策略 3：有界递增/递减模式

v += const（正常数），变量有上界类型标注 → 度量 upper_bound - v 每次递减 const，下界 0。这是策略 1 的退化情况，编译器在最前面快速处理。

6.5 策略 4：乘法缩放度量模板

v *= const（const > 1），变量有上下界类型标注。编译器内置对数度量模板 ceil(log_const(upper/v))，每次乘 const 度量减 1。

yaoxiang

mut i: Positive(i) = 1
while i < n {
    # 编译器自动推导：度量 ceil(log₂(n/i))，每次乘 2 度量减 1
    i *= 2
}

6.6 终止性与正确性分离

终止性证明和正确性证明是独立的：

终止性：以上四种策略自动证明循环在有限步内退出
正确性：循环体是否朝目标类型推进，由编译期证明管道通过验证条件检查

两者都通过 → 编译通过。终止性得证但正确性失败 → 编译错误 + 反例。正确性得证但终止性无法证明 → 编译错误并指出无法分析的变量或操作。两者都失败 → 编译错误分别报告两项失败原因。

6.7 递归函数的终止检查

对需要在编译期求值的递归函数，编译器检查参数递减：

yaoxiang

factorial: (n: Int) -> Int = {
    if n <= 1 { return 1 }
    return n * factorial(n - 1)  # 编译器分析：n-1 < n → 递减 → 终止
}

# 编译期使用——编译器保证 factorial 在编译期终止
vec: Vec(factorial(5)) = Vec(120)()  # 5! = 120，编译期完成

场景	行为
编译器能分析出递归递减（如 `n-1`）	编译期求值
不递减/无法判定递减	编译错误
运行时调用（非类型位置）	不需要终止检查

6.8 硬边界

i = f(i) 且 f 不可逆、不封闭、不保持任何单调性——数学上不可能自动证明终止。编译错误：

此循环无法自动证明终止。循环变量依赖于不可分析的函数 f。请使用可被编译器分析的迭代模式。

这不是编译器的失败。凡无法静态证明安全的代码，不得通过编译。

8. SMT 求解器：类型检查器的加速模块

SMT 求解器在传统语言中是外部工具（如 F* 调用 Z3，Dafny 调用 Z3）。在 YaoXiang 中，它是类型检查器的一个加速模块——仅当编译器内核自身无法直接判定时才被调用。SMT 帮忙找证明，但验证证明的是类型检查器。

信任模型：类型检查器是唯一的信任根。SMT 求解器是加速模块——它帮忙找证明，但 SMT 不是独立的信任边界。编译器信任 Z3 的 unsat 结果（与 F*/Dafny 路线一致——Z3 出错的概率低于编译器自身的 bug 率，是工程上的务实选择）。真正的不可靠性控制在 SMT 翻译层——如果翻译有 bug，编译器会在其他测试中暴露。

接口：编译器内部翻译为 SMT-LIB 2.6 标准格式，而非绑定特定求解器 API。SMT-LIB 是 ISO 标准，Z3、CVC5、MathSAT、Yices 全部原生支持。

默认后端：Z3（MIT 协议，最广泛的文档和社区验证）。CVC5 作为 SMT-LIB 兼容的备选——用户在编译时可以通过编译器标志切换。

不做"通用求解器抽象层"——SMT-LIB 就是抽象层。未来如果 CVC5 在特定理论上有突破，切换只需换二进制，不需改编译器代码。

编译期 Bool 表达式
        │
        ├── 编译器内核可直接判定（结构等价、简单算术、
        │   常量折叠后的平凡公式）
        │   → 直接返回 Proved / Disproved
        │
        └── 编译器内核无法直接判定（量词、符号变量）
            → 依赖类型预归约（factorial(5) → 120）
            → 翻译为 SMT-LIB 格式
            → 发送给 Z3/CVC5（带预算限制）
            → 返回值：unsat → Proved  │  sat + 模型 → Disproved  │  unknown → Unproven

求解预算——硬限制，像栈深度一样：

预算维度	默认值	说明
求解步数	10,000	Z3 对线性算术通常在百步以内。10,000 步覆盖 99% 的实际谓词。
时间	100ms	单谓词超过 100ms = 用户在写编译期程序而非类型标注。100ms × 50 个谓词 = 5 秒编译时间上限。
量词实例化深度	3	三层嵌套量词覆盖实际模式。超过三层大概率在写逻辑练习题。

超预算返回 Unproven，编译错误 + 谓词位置 + 消耗量。没有降级，没有运行时检查，没有 silent pass。

为什么这实际可行：工程中 95% 的实际谓词是线性算术——x > 0、arr.len > 0、0 <= idx < arr.len——全在可判定片段内，SMT 求解器对这类问题毫秒级返回。遇到极少数超预算的复杂谓词，程序员写证明函数即可。

依赖类型在 SMT 调用前做了一层预归约：factorial(5) 直接编译期求值得 120，append([1,2], [3]) 直接求值得 [1,2,3]。这些确定性的值计算不消耗 SMT 预算。

程序员不需要知道 SMT 的存在。心智模型是：编译器能证明就通过，不能就报错——如果编译器不会，你可以写个函数证明给它看。

9. 编译期谓词组合

编译期谓词是返回 Type 的函数，组合通过函数组合自然实现：

yaoxiang

SortedNonEmpty: (T: Ord, arr: Array(T)) -> Type = {
    Sorted(T, arr) && NonEmpty(arr)
}

10. 代码示例

9.1 除法安全

yaoxiang

Positive: (x: Int) -> Type = { x > 0 }

divide: (a: Int, b: Positive(b)) -> Int = a / b

result = divide(10, 2)   # ✅ 编译器验证 Positive(2) = { 2 > 0 } → True
# result = divide(10, 0)  # ❌ 编译器验证 Positive(0) = { 0 > 0 } → False

9.2 数组访问安全

yaoxiang

InBounds: (idx: Int, arr: Array(T)) -> Type = { 0 <= idx && idx < arr.len }

get: (arr: Array(T), idx: InBounds(idx, arr)) -> T = arr.data[idx]

arr = Array(Int)(1, 2, 3)
x = get(arr, 1)   # ✅ 编译器验证 InBounds(1, arr) = { 0 <= 1 && 1 < 3 } → True
# y = get(arr, 5)  # ❌ 编译器验证 InBounds(5, arr) = { 0 <= 5 && 5 < 3 } → False

9.3 排序正确性

yaoxiang

Sorted: (T: Ord, arr: Array(T)) -> Type = {
    forall i in 0..arr.len-1: arr[i] <= arr[i+1]
}

sort: (T: Ord) -> ((arr: Array(T))) -> (result: Sorted(T, result)) = {
    result = arr.clone()
    # ... 排序算法实现 ...
    return result
}

9.4 循环：编译器 VC 生成

yaoxiang

SumUpTo: (arr: Array(Int), i: Int) -> Type = { s: Int; s == sum(arr[0..i]) }
UpTo: (n: Int) -> Type = { i: Int; 0 <= i <= n }

sum: (arr: Array(Int)) -> Int = {
    mut s: SumUpTo(arr, i) = 0
    mut i: UpTo(arr.len) = 0
    while i < arr.len {
        s += arr[i]
        i += 1
    }
    return s
}

11. dispatch 分派管道：编译期与运行时的统一分派

assert 和 Assert 是同一个精化类型原语的两面。分派管道 dispatch 按谓词的自由变量在编译期是否可及自动决定走编译期证明还是运行时检查：

判据	模式	行为
所有自由变量编译期已知（泛型参数、编译期常量）	CompileTime	进证明管道：Proved → 擦除，Disproved → 编译错误，Unknown → 要求证明
存在自由变量来自运行时（函数参数、外部输入、mut 变量）	Runtime	插入运行时 check，并向流敏感假设集 Γ 注入精化事实

关键：「判不了」≠「证伪」。CompileTime 模式下 Unknown 要求证明（不静默降级），Runtime 模式下命题在编译期根本没有真假可言——prover 再强也无法为「用户可能输入了负数」写出恒真证明，运行时 check 是唯一 sound 选择。这不是 prover 不够强，是理论必然。

12. 流敏感假设集 Γ ：最强后置条件传播

编译器维护一个流敏感（flow-sensitive）假设集 Γ，跟踪每个控制流点已知成立的命题。

SP（最强后置条件）传播：

yaoxiang

assert(x > 0)       // Γ = {x > 0}
y = x + 1           // Γ = {x > 0, y > 1}  ← SP 传播

mut 变量的 kill set：mut 变量重新赋值后，涉及该变量的所有假设从 Γ 中移除：

yaoxiang

assert(x > 0)       // Γ = {x > 0}
mut x = x - 5       // Γ = {}  ← x > 0 被 kill

这是 soundness 的硬要求——变量值变了，旧假设无效。

分支合流：IF/ELSE 或 match 分支合并时，Γ 取各分支假设的交集。只有所有路径都成立的命题才带出分支。

13. 擦除模型澄清：witness 擦除 ≠ check 擦除

RFC-027 的「精化类型在运行时完全擦除」论断指的是 proof witness（证明令牌）——编译期已验证的证明项不产生运行时代码。但 Runtime 模式下 dispatch 插入的 运行时 check 是保留的——它是在值层面执行的 Bool 检查，不是类型层面的 witness。

总结：witness 擦除，check 保留。两件事不冲突，RFC-027 原论断不变。

详细设计

语法变化

之前 (RFC-022)	之后 (本 RFC)
`//! requires: NonEmpty(n) = n > 0`	编译期谓词作为参数类型 `(b: Positive(b))`
`//! ensures: ExistsMax(result, arr)`	返回类型使用返回值形参 `-> (result: IsMax(T, arr, result))`
`/! invariant: ... !/`	变量上的编译期谓词类型标注——Floyd-Hoare 不变式
`//! decreases: n`	编译器全自动推导度量函数
规约是注释	规约是类型系统

语法

编译期谓词没有新关键字。 {} 是证明空间，和现有类型定义语法完全一致。编译期谓词就是返回 Type 的函数——name: (params) -> Type = { 断言 }。使用时就是函数调用——Positive(b)、IsMax(T, arr, result)。

bnf

# 编译期谓词 = 返回 Type 的函数，{} 内为编译器验证的断言
# 使用现有函数/类型语法，无需新增 BNF 规则
predicate ::= identifier ':' params '->' 'Type' '=' '{' assertions '}'

新增语法概念：返回值形参——-> (name: Type) 中 name 是返回值形参。

返回值形参是 YaoXiang 在现有函数语法上引入的唯一一个语法概念。它的语义：

name 的值由 return 语句提供
name 仅存在于类型签名中，被后置条件谓词引用（如 -> (result: IsMax(T, arr, result))）
name 不进入函数体作用域，不出现在调用方
返回值形参可选——无后置条件时签名与普通函数完全一致（-> Int），不引入任何额外负担

引入它的理由：后置条件需要引用"函数将要返回的值"。在没有返回值形参的情况下，编译器只能通过特殊规则（如隐式变量 $result 或 __retval__）来让谓词引用返回值。返回值形参将这种引用显式化——它就是一个形参，只是值由 return 而非调用方提供。

证明函数不是新概念——它就是一个 YaoXiang 函数，其返回类型是被断言的命题。当编译器返回 Unproven 时，程序员提供证明函数，类型检查器以与验证任何函数返回类型完全相同的方式验证它。不需要新语法、新关键字、新规则。

类型系统影响

类型宇宙：编译期谓词位于 Type₂ 层——接受值返回 Type 的函数，与类型构造器层级相同
泛型交互：编译期谓词可带泛型参数，如 NonEmpty: (T: Type) -> (arr: Array(T)) -> Type
所有权交互：编译期谓词中的表达式遵守所有权规则，只能读不能写
类型推导：编译期谓词的参数参与 HM 类型推导

运行时表示

编译期谓词在运行时按 dispatch 分派结果处理：

CompileTime 模式（所有自由变量编译期已知）：证明通过后见证令牌（witness）完全擦除。Positive: (x: Int) -> Type = { x > 0 }——参数 b: Positive(5) 在运行时的表示就是 Int。精化条件 { 5 > 0 } 已通过，擦除。
Runtime 模式（存在运行时自由变量）：保留运行时 check——在值层面执行 Bool 检查，注入流敏感假设集 Γ。详见 §11 dispatch 分派管道和 §13 擦除模型澄清。

将编译期谓词放在类型位置（如 f(x: Positive(x))）不产生包装类型、不分配额外内存。但 x 来自运行时输入时，会插入运行时 Bool 检查。

与 ref 的交互约束：编译期谓词只能引用不可变借用或所有权已转移的值。引用可变借用的编译期谓词，编译器无法在编译期保证验证结果在运行时仍然成立——此类用法直接报编译错误。

编译器改动

解析器：编译期谓词使用标准函数语法，无需额外解析规则
编译期证明管道：统一 Proved/Disproved/Unproven 返回接口，自动策略选择
SMT 加速模块：SMT-LIB 2.6 翻译层，默认后端 Z3，CVC5 备选
类型检查器内核：推理规则实现——结构等价、βδι-规约、全称量词引入/消去。这是唯一的信任根，SMT 和程序员证明都经由此验证
验证条件生成：WP/SP 演算 + 循环不变式证明义务
错误报告：反例格式化 + 未解命题报告 + 源码位置关联

向后兼容性

✅ 未使用编译期谓词的代码完全不变
✅ 编译期谓词在 CompileTime 模式下零运行时开销，Runtime 模式下仅保留必要的 Bool 检查
⚠️ RFC-022 的 //! 语法不再支持——但 022 从未被实现，无迁移负担

权衡

优点

Curry-Howard 同构完整兑现：类型即命题，程序即证明，name: Proposition = Proof
统一性：编译期谓词与普通函数使用完全相同的语法，无概念分裂
SMT 透明：程序员不需要知道 SMT 的存在，心智模型与类型检查一致
渐进式采用：可从一个编译期谓词开始，逐步增加覆盖
最小运行时开销：CompileTime 模式零开销，Runtime 模式仅保留必要的 Bool 检查

缺点

编译时间：SMT 求解增加编译时间，但预算硬限制保证上限可控
自动证明边界：超越一阶线性算术的复杂谓词可能需要程序员写证明函数。这不是语言缺陷——这是停机问题的必然结论。编译器诚实报告 Unproven 而非伪报 True/False
学习曲线：编写有效的编译期谓词和证明函数需要理解 Curry-Howard 同构的基本直觉
实现复杂度：编译期证明管道的统一需要精心设计

风险缓解

SMT 求解预算硬限制（步数 10,000 / 时间 100ms / 实例化深度 3），超预算返回 Unproven
依赖类型预归约：确定性的值计算先吃掉，SMT 只啃非确定部分
Unproven 不是死路：程序员可以写证明函数，类型检查器验证——和验证任何函数返回类型一致
增量验证：仅验证变更模块
清晰的错误信息 + 反例展示 + 预算消耗报告 + 未解命题 + 建议（如果编译器能给出）

替代方案

方案	为什么不选择
RFC-022：`//!` 注释式规约	规约与类型分裂，违反 Curry-Howard 同构
独立规约文件（如 CVL）	规约与代码分离，增加维护成本
仅运行时断言	无法静态保证正确性
外部证明助手（如 Coq）	与编译器割裂，需要独立的证明语言和信任边界。YaoXiang 的选择：证明就是 YaoXiang 代码，类型检查器是唯一信任根
本方案：编译期谓词作为一等公民	✅

实现策略

阶段划分

阶段	内容
阶段 1	编译器内核：结构等价 + βδι-规约 + 全称量词引入/消去。支持简单算术谓词（`x > 0`、`arr.len > 0`）
阶段 2	SMT-LIB 翻译层 + Z3/CVC5 集成。管道返回 Proved/Disproved/Unproven。Unproven 时支持程序员写证明函数
阶段 3	循环不变式 VC 生成 + 终止检查（线性秩函数 + 谓词违反计数 + 有界模式 + 组合爆炸控制）
阶段 4	增量验证 + 缓存 + IDE 支持

依赖关系

RFC-010: 统一类型语法 — 编译期谓词基于 name: type = value
RFC-011: 泛型系统 — 编译期谓词可带泛型参数
RFC-009: 所有权模型 — 编译期谓词表达式遵守所有权规则

开放问题

[x] SMT 求解器选择：默认 Z3（MIT 协议，最广泛验证）。CVC5 作为 SMT-LIB 兼容备选，编译器标志切换。编译器内部翻译目标为 SMT-LIB 2.6 标准格式——SMT-LIB 就是抽象层，不做自定义通用求解器接口。
[x] 求解预算的具体数值：步数 10,000 / 时间 100ms / 量词实例化深度 3。编译器内部固定，不给 knob。实际使用中如有真实用例证明不够（非"用户写错了"），再调整。
[x] 量词支持范围：语言层面不限制量词阶数。编译期谓词接受 Type 参数——Type 包括函数类型——因此高阶量词是类型系统的自然推论，不需要特殊语法。SMT 求解器可自动判定一阶量词（forall/exists，支持交错嵌套，由预算深度 3 限制）。高阶量词：SMT 返回 Unproven，编译器提示"此谓词超出自动证明范围，请提供证明函数"。程序员写一个返回类型等于该命题的 YaoXiang 函数——类型检查器验证该函数。不需要外部导出，不需要 AI，不需要交互式证明模式。一切都是 YaoXiang 代码，一切由类型检查器验证。
[x] 反例格式化：源码变量名直接用作 SMT 变量名（加上模块前缀避免冲突）。Z3 模型返回时按变量名反查。输出格式：变量名 = 具体值 + 源码位置 + 谓词定义位置。不做复杂映射层。
[x] ~~与 ref 智能指针的编译期谓词交互？~~ → 已决策：编译期谓词只允许不可变借用或已转移所有权的值。可变借用的值不可出现在编译期谓词中。
[x] forall 谓词违反计数量度对非相邻操作的扩展？ → 不扩展。当前覆盖范围（相邻交换、相邻移动）由策略 1（线性秩函数）互补覆盖——快排外层区间收缩由策略 1 兜底，堆排序由策略 1（数组索引模式）兜底。不能由任何策略证明终止的循环，编译器直接报错——这是硬安全哲学，不是缺陷。如果未来有真实场景（非学术构造）的算法四种策略都无法覆盖，再重新讨论。
[x] 线性秩函数枚举组合爆炸：候选枚举上限为 3 个有界变量。≤3 时枚举所有线性组合并 SMT 逐一验证。>3 时只尝试单变量度量（v_i、u_i - v_i），失败直接报编译错误——提示程序员"循环有 >3 个有界变量，编译器无法自动合成多变量度量"。这不是工程妥协——是迫使程序员写更简单的循环。

参考文献

RFC-010: 统一类型语法
RFC-011: 泛型系统设计
RFC-009: 所有权模型
Howard, W. A. (1969). The Formulae-as-Types Notion of Construction.
Swamy, N. et al. (2016). Dependent Types and Multi-Monadic Effects in F*. POPL 2016.
Vazou, N. et al. (2014). Refinement Types for Haskell. ICFP 2014.
Leino, K. R. M. (2010). Dafny: An Automatic Program Verifier for Functional Correctness. LPAR 2010.
De Moura, L. & Bjørner, N. (2008). Z3: An Efficient SMT Solver. TACAS 2008.

生命周期与归宿

┌─────────────┐
│   草案      │  ← 作者创建
└──────┬──────┘
       │
       ▼
┌─────────────┐
│  审核中     │  ← 当前状态：社区讨论
└──────┬──────┘
       │
       ├──────────────────┐
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│  已接受     │    │  已拒绝     │
└──────┬──────┘    └──────┬──────┘
       │                  │
       ▼                  ▼
┌─────────────┐    ┌─────────────┐
│ accepted/   │    │  rejected/  │
│ (正式设计)  │    │ (保留原位)  │
└─────────────┘    └─────────────┘

RFC-027：编译期谓词与统一静态验证 ​

摘要 ​

动机 ​

为什么废弃 RFC-022？ ​

当前的问题 ​

正确的心智模型 ​

提案 ​

1. {} 是证明空间：类型即断言，验证即类型检查 ​

2. 前置/后置条件：参数类型和返回类型上的编译期谓词 ​

3. 路径条件传播：运行时值的编译期验证 ​

3.1 显式函数调用 ​

3.2 路径条件收集 ​

3.3 假设栈 ​

3.4 无静态证据则编译错误 ​

3.5 与统一管道的关系 ​

4. 编译期证明管道 ​

4.1 证明结果：三值代数 ​

4.2 Unproven 之后：程序员写证明 ​

4.3 管道内的分层依赖 ​

5. 三层函数统一 ​

6. 循环：Floyd-Hoare 验证条件生成 ​

6.1 依赖追踪：可变变量上的依赖类型 ​

7. 终止检查 ​

6.1 设计原则 ​

6.2 策略 1：线性秩函数自动合成 ​

6.3 策略 2：谓词违反计数——从目标类型自动提取度量 【实验性策略】 ​

6.4 策略 3：有界递增/递减模式 ​

6.5 策略 4：乘法缩放度量模板 ​

6.6 终止性与正确性分离 ​

6.7 递归函数的终止检查 ​

6.8 硬边界 ​

8. SMT 求解器：类型检查器的加速模块 ​

9. 编译期谓词组合 ​

10. 代码示例 ​

9.1 除法安全 ​

9.2 数组访问安全 ​

9.3 排序正确性 ​

9.4 循环：编译器 VC 生成 ​

11. dispatch 分派管道：编译期与运行时的统一分派 ​

12. 流敏感假设集 Γ ：最强后置条件传播 ​

13. 擦除模型澄清：witness 擦除 ≠ check 擦除 ​

详细设计 ​

语法变化 ​

语法 ​

类型系统影响 ​

运行时表示 ​

编译器改动 ​

向后兼容性 ​

权衡 ​

优点 ​

缺点 ​

风险缓解 ​

替代方案 ​

实现策略 ​

阶段划分 ​

依赖关系 ​

开放问题 ​

参考文献 ​

生命周期与归宿 ​

RFC-027：编译期谓词与统一静态验证

摘要

动机

为什么废弃 RFC-022？

当前的问题

正确的心智模型

提案

1. `{}` 是证明空间：类型即断言，验证即类型检查

2. 前置/后置条件：参数类型和返回类型上的编译期谓词

3. 路径条件传播：运行时值的编译期验证

3.1 显式函数调用

3.2 路径条件收集

3.3 假设栈

3.4 无静态证据则编译错误

3.5 与统一管道的关系

4. 编译期证明管道

4.1 证明结果：三值代数

4.2 Unproven 之后：程序员写证明

4.3 管道内的分层依赖

5. 三层函数统一

6. 循环：Floyd-Hoare 验证条件生成

6.1 依赖追踪：可变变量上的依赖类型

7. 终止检查

6.1 设计原则

6.2 策略 1：线性秩函数自动合成

6.3 策略 2：谓词违反计数——从目标类型自动提取度量【实验性策略】

6.4 策略 3：有界递增/递减模式

6.5 策略 4：乘法缩放度量模板

6.6 终止性与正确性分离

6.7 递归函数的终止检查

6.8 硬边界

8. SMT 求解器：类型检查器的加速模块

9. 编译期谓词组合

10. 代码示例

9.1 除法安全

9.2 数组访问安全

9.3 排序正确性

9.4 循环：编译器 VC 生成

11. dispatch 分派管道：编译期与运行时的统一分派

12. 流敏感假设集 Γ ：最强后置条件传播

13. 擦除模型澄清：witness 擦除 ≠ check 擦除

详细设计

语法变化

语法

类型系统影响

运行时表示

编译器改动

向后兼容性

权衡

优点

缺点

风险缓解

替代方案

实现策略

阶段划分

依赖关系

开放问题

参考文献

生命周期与归宿