⚠️ 已废弃 (DEPRECATED)
本 RFC 已被 RFC-027：编译期求值类型与统一静态验证 取代。
废弃原因：022 将规约设计为 //! 注释形式的外挂语法，这与 Curry-Howard 同构的根本原则相悖——"没有 //! 注释。没有独立的规约语言。一切都在类型系统内。"新设计将编译期求值类型作为一等公民，通过统一的编译期 Bool 求值管道替代了注释式规约。Debug/Release 的分裂验证模式也被统一的 True/False/Unknown 三级返回值模型取代。
本文档仅作历史参考保留。

RFC 022: 霍尔逻辑静态验证支持（规约注释与规约类型）[已废弃]

参考:
RFC-010: 统一类型语法
RFC-011: 泛型系统设计
RFC-009: 所有权模型

摘要

本文提出为 YaoXiang 语言引入一种霍尔逻辑静态验证机制，允许开发者在注释中以 //! 或 /*! ... !*/ 的形式编写前置条件、后置条件和循环不变式。在 Debug Build 时进行强制静态验证，验证通过后才能进行 Release Build；Release Build 时忽略规约注释（零开销）并清除验证缓存。规约本身被视为类型系统的一部分，形成"规约类型"（如 Requires(P)、Ensures(P)），并可被用户扩展。该设计旨在保持语言简洁的同时，为关键代码提供高可靠性保障，且与 YaoXiang 的统一类型模型完美融合。

动机

为什么需要这个特性/变更？

YaoXiang 已经通过所有权模型（RFC-009）和并发模型（RFC-001）保证了内存安全和线程安全，但逻辑正确性仍依赖测试。对于系统编程、安全关键领域（如航天、金融、操作系统内核），逻辑错误可能导致灾难性后果。现有方案（如 Rust 的借用检查）无法捕获这类错误。霍尔逻辑提供了一种数学证明手段，但传统形式化验证工具往往需要独立的规约语言和复杂的学习曲线。

当前的问题

逻辑正确性只能通过测试验证，无法在编译期保证
关键系统代码缺乏形式化验证手段
现有形式化验证工具学习曲线陡峭，与主流编程语言割裂

提案

核心设计

我们的目标是设计一种轻量、与语言一体的静态验证方案：

Debug Build 必验证：开发者在需要高可靠性的模块中编写规约，Debug Build 时强制验证通过后才能进行 Release Build
语法优雅：使用 //! 注释，不引入新关键字，且能被编辑器染色识别
与类型系统融合：规约成为类型的一部分，可参与类型检查，支持用户自定义规约类型
可证明与可测试：既可静态证明，也可降级为运行时断言，便于渐进式采用

1. 规约注释语法

在函数体或循环体的开头，使用 //!（单行）或 /*! ... !*/（多行）编写规约。

1.1 统一规约语法

规约采用 YaoXiang 统一的 name: Type = expression 语法模型，与类型系统完全融合：

yaoxiang

max: (T: Ord) -> ((arr: Array(T, n)) -> T) = {
    //! requires: NonEmpty(n) = n > 0
    //! ensures: GreaterOrEqual(result, arr[0..n])
    //! ensures: ExistsMax(result, arr[0..n])
    // 实现...
}

规约本质是一个类型声明，右侧是布尔表达式
左侧是规约类型实例（可带类型参数）
可使用特殊变量 result 表示返回值

1.2 循环规约

yaoxiang

while i < n {
    /*! invariant: Bounds[i, n] = 0 <= i <= n
                  && SumInvariant[s, arr[0..i]] !*/
    s = s + arr[i]
    i = i + 1
}

1.3 规约表达式

规约右侧的布尔表达式使用 YaoXiang 表达式语法，支持：

算术运算、比较运算、逻辑运算
量词：forall i in 0..n: P(i)、exists i in 0..n: P(i) — 语言内置的逻辑构造
函数调用（必须是纯函数）

2. 规约类型系统

规约类型本质上是 YaoXiang 的普通类型，与统一语法模型完全一致。

2.1 内置规约类型

编译器内置以下常用规约类型（可在规约中直接使用）：

yaoxiang

// 内置规约类型定义
NonEmpty: (T: Type) -> Type = { len: T; len > 0 }
Positive: Type = { x: Int; x > 0 }
GreaterOrEqual: (T: Type) -> Type = { result: T, arr: Array(T); result >= arr[0] && forall i in 1..arr.len: result >= arr[i] }
Bounds: (T: Type) -> Type = { i: T, n: T; 0 <= i && i <= n }
SumInvariant: (T: Type) -> Type = { s: T, arr: Array(T); s == sum(arr[0..i]) }

// 量词构造（语言内置，非函数）
forall: (start: Int, end: Int, pred: (Int) -> Bool) -> Bool
exists: (start: Int, end: Int, pred: (Int) -> Bool) -> Bool

2.2 用户自定义规约类型

与普通类型定义完全一致，用户可自定义规约类型：

yaoxiang

// 定义正整数规约
Positive: Type = { x: Int; x > 0 }

// 定义已排序数组规约
Sorted: (T: Ord) -> Type = {
    arr: Array(T);
    forall i in 0..arr.len-1: arr[i] <= arr[i+1]
}

// 定义最大值规约
ExistsMax: (T: Ord) -> Type = {
    result: T, arr: Array(T);
    exists i in 0..arr.len: result == arr[i]
    && forall j in 0..arr.len: result >= arr[j]
}

使用自定义规约：

yaoxiang

sqrt: (x: Positive) -> Float = {
    //! ensures: SquareRootResult(result, x) = result * result <= x && (result+1)*(result+1) > x
    // 实现...
}

binary_search: (T: Ord) -> ((arr: Sorted(Array(T)), key: T) -> Option(Index)) = {
    //! ensures: SearchResult(result, arr, key)
    // 实现...
}

规约类型与其他类型一样，支持泛型参数、类型约束，可参与类型推导。

3. 编译模式

模式	行为	选项
Debug Build	解析规约，生成验证条件，调用 SMT 求解器证明；验证通过后才能进行 Release Build	`yaoxiangc --debug source.yx`
Release Build	忽略所有 `//!` 注释，不生成任何代码；清除所有验证缓存；启用激进优化	`yaoxiangc --release source.yx`
运行时检查	将规约转换为运行时断言，违反时 panic	`yaoxiangc --enable-runtime-checks source.yx`

验证模式下，如果证明失败，编译器将报告错误，并提供可能的反例（如输入值）。

4. 验证机制

编译器将规约转换为验证条件（Verification Conditions），并发送给集成的 SMT 求解器（如 Z3）。验证过程大致如下：

收集函数的 requires 和 ensures，循环的 invariant
为每个循环生成循环不变式证明义务：进入循环前成立，每次迭代后保持，循环退出后蕴含后置条件
将函数体转化为逻辑公式，结合规约，形成验证条件
调用 SMT 求解器检查可满足性

如果求解器返回 unsat（不可满足），则规约成立；否则报告反例。

5. 与测试的结合

运行时检查模式可将规约转换为断言，用于测试。结合规约覆盖率工具，可以评估测试对规约的覆盖程度。未来可考虑规约挖掘工具，从测试中自动推断候选规约。

6. 编辑器支持

//! 和 /*! ... !*/ 可被编辑器识别为特殊注释，赋予不同颜色（如紫色），与普通注释区分。语言服务器可提供规约的悬停提示、补全和验证错误报告。

详细设计

语法变化

之前	之后
无规约注释语法	允许 `//!` 和 `/! ... !/` 规约注释

7.1 语法扩展

在现有语法（RFC-010）基础上，允许在函数体和循环体开头出现零条或多条 //! 或 /*! ... !*/ 注释。规约语法与统一类型语法一致：

spec_comment     ::= ('//!' spec_line) | ('/*!' spec_block '!*/')
spec_line        ::= spec_name ':' type_expr '=' expr
spec_name        ::= 'requires' | 'ensures' | 'invariant'
spec_block       ::= (spec_name ':' type_expr '=' expr ';')*

规约本质是类型声明：规约名: 规约类型 = 布尔表达式
type_expr 是规约类型表达式，可带类型参数
expr 使用 YaoXiang 表达式语法，支持量词

7.2 类型检查

在验证模式下，编译器将规约注释转换为对应的规约类型实例，并记录在函数或循环的元数据中。

7.3 验证条件生成

采用 weakest precondition 或 strongest postcondition 演算，结合循环不变式，生成一阶逻辑公式。生成的 VC 使用 SMT-LIB 格式，调用外部求解器。

7.4 错误报告

如果证明失败，求解器可能提供模型（反例）。编译器应将这些反例转换为可读的形式，例如具体的输入值，帮助用户调试。

7.5 运行时检查

在 --enable-runtime-checks 模式下，编译器将规约转换为 assert 语句：

requires：在函数入口插入 assert(cond)
ensures：在函数所有返回点之前插入 assert(cond)，其中 result 替换为实际返回值
invariant：在循环体开头插入 assert(cond)

7.6 与现有设计集成

所有权模型：规约中的表达式遵守所有权规则，只能读不能写（纯函数），避免副作用
泛型系统：规约类型支持泛型参数（如 Requires(P)），可与泛型函数/类型结合
依赖类型：规约中的值依赖类型（如数组长度 n）自然可用

类型系统影响

规约类型是 YaoXiang 的普通类型，与统一语法模型一致
编译器内置常用规约类型（Positive、NonEmpty、GreaterOrEqual 等）
用户可通过普通类型定义自定义规约类型
规约类型可带泛型参数，支持类型约束

运行时行为

Debug Build：调用 SMT 求解器进行静态验证，编译时间增加；验证成功后缓存验证结果
Release Build：规约注释被忽略，零运行时开销；清除所有验证缓存；启用 Span 缓存清除等激进优化
运行时检查模式：生成 assert 语句，运行时检测违规

编译器改动

解析器：识别规约注释语法
语义分析：收集规约，转换为规约类型
验证后端：生成验证条件，调用 SMT 求解器
代码生成：支持运行时检查模式

向后兼容性

✅ 完全向后兼容
规约注释在普通编译下被忽略，不影响现有代码
Release Build 时规约被忽略，无额外开销

权衡

优点

Debug Build 验证：Debug Build 时强制验证，确保逻辑正确
语法优雅：纯注释，无新关键字，编辑器友好
与类型系统融合：规约即类型，可扩展
渐进式采用：可从运行时检查逐步过渡到静态验证
可靠性提升：能捕获测试难以发现的逻辑错误

缺点

编译时间：验证模式可能显著增加编译时间
学习曲线：需要学习如何编写有效的规约和量词
SMT 求解器局限性：某些复杂性质可能无法自动证明

替代方案

方案	优点	缺点
新关键字（如 `requires`）	语法直观	引入新关键字，破坏简洁性
独立的规约文件（如 CVL）	规约与代码分离	增加文件数量，难以同步
仅运行时断言	实现简单	无法静态保证
本方案（注释+规约类型）	平衡简洁与功能	需编辑器支持

实现策略

阶段划分

阶段	内容
阶段 1：基础支持	扩展解析器，识别 `//!` 和 `/! ... !/` 注释，将其附加到 AST 节点；在验证模式下收集规约，生成简单的验证条件（仅算术比较）；集成 Z3 求解器
阶段 2：量词支持	支持量词表达式，翻译为 SMT-LIB 的 `forall`/`exists`；提供规约的 IDE 高亮和悬停提示
阶段 3：优化与工具链	增量验证，缓存已验证的模块；规约覆盖率报告；规约挖掘工具（从测试生成候选规约）

依赖关系

RFC-009: 所有权模型 - 规约表达式需要纯函数语义
RFC-010: 统一类型语法 - 规约类型系统基于类型系统
RFC-011: 泛型系统设计 - 规约类型支持泛型参数

风险

SMT 求解器集成复杂性：Z3 等求解器的集成可能遇到技术挑战
- 缓解：使用成熟的 Rust Z3 bindings，逐步扩展支持的表达式类型
验证失败调试困难：当 SMT 求解器无法证明规约时，用户可能难以理解原因
- 缓解：提供清晰的错误信息和反例解释
性能开销：验证模式可能显著增加编译时间
- 缓解：实现增量验证和缓存机制

开放问题

[ ] 量词支持范围：是否支持嵌套量词？是否支持高阶量词？
[ ] 循环不变式推断：是否提供自动推断简单不变式的功能？
[ ] 证明失败反例格式：如何呈现反例最为有效？
[ ] 与其他验证工具集成：是否考虑与 Coq、Lean 等证明助手集成？

参考文献

生命周期与归宿

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

状态说明

状态	位置	说明
草案	`docs/design/rfc/`	作者草稿，等待提交审核
审核中	`docs/design/rfc/`	开放社区讨论和反馈
已接受	`docs/design/accepted/`	成为正式设计文档，进入实现阶段
已拒绝	`docs/design/rfc/`	保留在 RFC 目录，更新状态

接受后的操作

将 RFC 移至 docs/design/accepted/ 目录
更新文件名为描述性名称（如 hoare-logic-static-verification.md）
更新状态为 "正式"
更新状态为 "已接受"，添加接受日期

拒绝后的操作

保留在 docs/design/rfc/ 目录
在文件顶部添加拒绝原因和日期
更新状态为 "已拒绝"

RFC 022: 霍尔逻辑静态验证支持（规约注释与规约类型）[已废弃] ​

摘要 ​

动机 ​

为什么需要这个特性/变更？ ​

当前的问题 ​

提案 ​

核心设计 ​

1. 规约注释语法 ​

1.1 统一规约语法 ​

1.2 循环规约 ​

1.3 规约表达式 ​

2. 规约类型系统 ​

2.1 内置规约类型 ​

2.2 用户自定义规约类型 ​

3. 编译模式 ​

4. 验证机制 ​

5. 与测试的结合 ​

6. 编辑器支持 ​

详细设计 ​

语法变化 ​

7.1 语法扩展 ​

7.2 类型检查 ​

7.3 验证条件生成 ​

7.4 错误报告 ​

7.5 运行时检查 ​

7.6 与现有设计集成 ​

类型系统影响 ​

运行时行为 ​

编译器改动 ​

向后兼容性 ​

权衡 ​

优点 ​

缺点 ​

替代方案 ​

实现策略 ​

阶段划分 ​

依赖关系 ​

风险 ​

开放问题 ​

参考文献 ​

生命周期与归宿 ​

状态说明 ​

接受后的操作 ​

拒绝后的操作 ​

RFC 022: 霍尔逻辑静态验证支持（规约注释与规约类型）[已废弃]

摘要

动机

为什么需要这个特性/变更？

当前的问题

提案

核心设计

1. 规约注释语法

1.1 统一规约语法

1.2 循环规约

1.3 规约表达式

2. 规约类型系统

2.1 内置规约类型

2.2 用户自定义规约类型

3. 编译模式

4. 验证机制

5. 与测试的结合

6. 编辑器支持

详细设计

语法变化

7.1 语法扩展

7.2 类型检查

7.3 验证条件生成

7.4 错误报告

7.5 运行时检查

7.6 与现有设计集成

类型系统影响

运行时行为

编译器改动

向后兼容性

权衡

优点

缺点

替代方案

实现策略

阶段划分

依赖关系

风险

开放问题

参考文献

生命周期与归宿

状态说明

接受后的操作

拒绝后的操作