code-contracts

代码契约

一种简单的开放格式，用于指定与代码共置的结构化假设和要求，从而支持更快、更出色的 Agent 驱动软件开发。

/**
 * @cc [owner:spolu,label:product] balance-pre-and-fail
 * `from.balance` is expected to be greater than or equal to `invoice.amount`, fails with
 * `InsufficientBalanceError` otherwise.
 */
/**
 * @cc [owner:spolu,label:product] balance-post
 * `from.balance` is decreased by `invoice.amount` and `invoice.status` is set to `paid`.
 */
/**
 * @cc [owner:spolu,label:product] atomicity
 * The operation is atomic: either `from.balance` is decreased and `invoice.status` is set to
 * `paid`, or neither is changed.
 */
export async function payInvoice(
  invoice: Invoice,
  from: Account,
): Promise<PaidInvoice> {
 ...
}

为什么需要代码契约？

代码契约由人类和 Agent 编写并使用，帮助他们推理代码。

代码契约主要有三种用途：

规范：与独立的产品或系统规范文件相比，代码契约嵌入在代码附近，不易偏离代码，也更容易发现。人类可以借助代码契约推理行为，而无需检查实现细节。Agent 则利用它们指导实现，并向人类和后续 Agent 展示重要假设。

注意力：代码契约以结构化方式呈现重要假设和不变量，减少推理代码所需的反复过程，从而释放现代软件开发团队中最紧缺的资源之一：人类的注意力。

验证：代码契约的结构和粒度使工具能够强制执行合规性，并简化长期维护。代码契约执行情况可为 Agent 提供验证信号，从而提升其性能。

代码契约能够实现：

• 让人类开发者与编码 Agent 更高效地协作。
• 生成式代码分析与验证，提升 Agent 性能。
• 在代码层面大规模维护不变量、产品契约和安全假设。

工具

npm install --global @spolu/cc-check

cc-check 命令行界面提供：

• cc-check format [file-like]：报告受支持的源文件或 CONTRACTS 文件中格式错误的 @cc 语法和重复的契约 ID。如果未指定路径，则递归检查当前目录中的每个受支持文件。它不会重写文件，也不会评估契约文本或实现是否合规。
• cc-check list <file-like|location-like>：列出附加到受支持源文件中各声明的契约，或适用于包含某个源代码位置的声明及其声明祖先的契约。默认包括祖先 CONTRACTS 文件中适用于目录范围的契约；传入 --no-global 可将其排除。

cc-check format
cc-check format path/file.rs
cc-check list path/to/file.ts:42
cc-check list path/to/file.go

规范与语法

@cc 指令从任何受支持源语言的文档注释中提取。每条指令定义一个代码契约。契约通常与函数、类或方法定义并列，或位于其中。

未附加到声明的代码契约位于名为 CONTRACTS 的文件中。这些契约适用于该文件所在目录及其后代目录中的所有代码。其典型用途是表达目录范围的编码规则，例如架构边界、依赖约束或安全实践。

CONTRACTS 文件示例：

@cc [owner:spolu,label:architecture] database-access-thru-resources
Database accesses must happen exclusively through `Resource`-like interfaces.

@cc [owner:spolu,label:security] no-sensitive-data-logging
Credentials, tokens, secrets and user data must not be logged.

语法采用 ISO 风格的 EBNF。SP 表示一个或多个空格，NL 表示换行符。解析前会移除注释分隔符和装饰符，例如 /**、*/、//、///、Python 文档字符串的三引号，以及行首的 *。

contracts_file
              = { contract, NL } ;
contract      = directive, NL, prose ;
directive     = "@cc", SP, [ metadata, SP ], contract_id ;

metadata      = "[", attribute, { ",", attribute }, "]" ;
attribute     = key, ":", value ;

contract_id   = token ;
key           = token ;
value         = token ;
prose         = prose_line, { NL, prose_line } ;

token 是不含空白、逗号、冒号或方括号的非空序列。元数据键可扩展；owner、notify 和 label 是常用键。一个契约可以有多个所有者、通知接收人和标签。建议使用 ; 分隔属性中的值，而不是重复键： 使用 [owner:spolu;tdraier,label:product]，而不是 [owner:spolu,owner:tdraier,label:product]；多个标签则使用 label:product;security。 重复键仍然有效。分号分隔的列表是一种元数据约定；解析器会将每个值保留为单个 token。prose_line 是任何不以 @cc 指令开头的行。

owner 列出 GitHub 用户名，当现有契约被修改或删除时会通知这些用户。新增契约时不会通知所有者。notify 列出 GitHub 用户名，每次发现违反该契约的情况时都会通知这些用户。 例如，[owner:spolu,notify:spolu;flvndvd,label:product] 会在契约变更时通知 spolu，在发现违规时通知 spolu 和 flvndvd。所有者不会自动收到违规通知；若他们也希望收到此类通知，请将其加入 notify。审查 Agent 会拆分分号分隔的列表、合并重复键，并去重用户名。

正文不能为空，内容延伸至文档注释末尾、CONTRACTS 文件中的下一条 @cc 指令，或该文件末尾。正文可以包含任意文本，且可以跨任意多行。核心格式不规定词汇、句式、情态或需求表示法，但通常应使用 Markdown。

一条文档注释包含一条 @cc 指令。多个连续的契约注释可以附加到同一个声明。契约 ID 在其所附加的声明范围内必须唯一且稳定；不同声明可以使用相同的 ID。CONTRACTS 文件中的契约不附加到任何声明，其 ID 在该文件及所有父级 CONTRACTS 文件中必须唯一且稳定。

附加契约的标识由其声明的语言特定标识和契约 ID 组成。目录契约的标识由其 CONTRACTS 文件相对于仓库的路径和契约 ID 组成。

代码契约工作流

对于 $code-contracts verify，请遵循按需验证。

发现契约

在更改或审查代码之前，手动或使用 cc-check list，找出约束目标代码的所有本地契约、封闭声明契约和祖先目录 CONTRACTS 文件中的义务。解析被调用的符号并检查其契约：调用可能违反在其他文件中声明的契约。

将所有适用的本地契约和目录契约视为同时生效的义务。若契约彼此冲突、已过时或无法实现，应明确指出，而不是默默择其一。文档示例和有意构造的格式错误测试样例不是生产环境中的契约声明。

编写契约

当代码契约简单、简洁且精确时，效果最好。针对特定声明的契约，应放在该语言支持的文档注释或文档字符串中。针对目录树的契约，应放在 CONTRACTS 中，通常用于架构、安全或编码约束。使用范围最窄的相关声明或目录边界。

每个源代码文档块中只能包含一个契约。契约 ID 在其声明范围内必须唯一且稳定。CONTRACTS 中的 ID 在该文件及其父级 CONTRACTS 文件中必须唯一且稳定。将 owner 设置为当前用户的 GitHub 用户名；如果可以获取其经过身份验证的 GitHub 身份，则使用该身份；无法确定时，应询问而不是猜测。可以有多个所有者；建议在单个 owner 属性中用 ; 分隔他们的用户名。多个标签和 notify 接收者也使用相同约定。只有在用户明确要求时才设置 notify；不要根据 owner 推断。遵循仓库既有的元数据约定。

使用 cc-check format 验证契约语法。该命令仅报告语法错误和重复 ID，无法证明文字内容属实，也无法证明代码符合契约。你有责任验证契约的有效性与一致性，以及代码是否符合契约。使用 cc-check list 验证契约是否易于查找。

围绕具体义务编写每个契约：

• 指出契约要防止的回归。 举出一种可能违反要求的变更。只描述函数用途的内容应放在普通文档中。
• 陈述可观察的要求。 优先采用“[条件，] 主体 MUST/MUST NOT 满足要求”的形式。直接陈述不变量同样有效；仅使用规范性关键词并不能让文字变得精确。
• 拆分彼此独立的义务。 每项要求使用一个契约。定义同一项要求的条件分支可以共用一个契约。
• 明确关键情形。 如果缺失数据、回退、错误或副作用行为会决定是否合规，就应将其写明。区分未返回结果与无法获取结果。
• 精确定义边界。 指明相关输入、输出、字段、状态或影响。若确有此意，应将“整个工作区范围”等表述转化为明确的前置条件或保证。
• 在不同实现间保留原意。 除非用途说明、理由和算法描述会施加实际约束，否则应将其省略。没有意图依据时，不要把偶然的实现行为提升为要求。

保留契约前，应确认审查者能够指出一种具体违规行为，以及一种符合契约的替代实现。

强制执行契约

你必须始终确保，所有发现的以及因代码更改而引入的契约都有效、一致、得到执行并受到遵守。契约没有自动语义强制机制。假定代码更改符合所有适用契约，因此作者和审阅者必须验证是否符合要求。

必须修复任务范围内的契约违规和矛盾，或清楚地指出。进行审查时，请遵循按需验证。

当行为有意改变时，须在同一更改中更新相关契约。验证契约变更对相关声明的使用者造成的影响。

所有代码更改的关键要求

• 在选择技术设计前，发现并审查适用契约。
• 为新行为引入相关契约。
• 当对现有代码作出重大假设时，补充缺失的契约。
• 更新或移除与行为变更相关的契约。
• 每次有意义的更改后，协调实现、相关测试和契约说明。
• 当行为有意改变时，如果契约规范的变更属于本次范围，须在同一更改中更新契约。
• 切勿仅为让实现看起来符合要求而删除或弱化契约。
• 将代码与契约不一致视为一项发现。修复或清楚地指出；不要假定任一方必然正确。

按需验证

当通过 $code-contracts verify 调用，或审查工作流要求执行此流程时，进行只读契约审查。阅读适用的仓库说明。除非另行要求，否则不要编辑文件、发布审查意见或发送通知。

使用指定的 PR、修订范围、文件、目录或仓库作为范围。如果未明确指定范围，则审查当前任务的更改，包括已提交的分支更改，以及已暂存、未暂存和未跟踪的文件。根据任务或仓库上下文推断分支的比较基准；如果无法确定目标或基准，则询问范围。可以不查看差异，直接依据当前契约验证文件或目录。如果工作流提供了已捕获的提交，则使用该确切比较范围，即使分支已更新。

差异相关性。 根据所有适用契约检查更改。检查未变更的代码，但只有当其与变更行为、该变更所依赖的假设，或新引入或修改的契约直接相关时，才报告既有违规。说明这种关联。仅处于同一文件、声明或调用图中并不足以构成相关性。此规则同样适用于先前审查中保留的发现。

无差异审计应覆盖所选范围的全部内容。

1. 检查差异和周边实现；如果没有适用的差异，则检查所选代码的完整内容。 对于提交比较，使用 git diff --find-renames <merge_base> <head_sha>，并使用 git show <merge_base>:<path> 检查旧代码和契约。若本地更改在范围内，也要纳入检查。 即使提供的文件列表可能被截断，也要在本地找出所有更改的文件。检查新增、修改内容以及删除造成的影响。 比较完整的契约正文和元数据；仅搜索新增的 @cc 行会漏掉纯文本更改和已删除的契约。
2. 对范围内的代码应用发现契约中的方法。使用 cc-check format 验证相关 契约语法。该命令只检查语法，不验证语义有效性或合规性。 如果调用方提供了 cc-check 可执行文件，请使用它。如果无法使用工具，请手动检查契约，并说明由此产生的验证限制。
3. 根据适用契约检查每个代码元素。追踪实际输入、守卫条件、错误、输出、状态更改和副作用。检查契约是否有效，以及是否与实现和其他适用契约一致。报告矛盾和有证据支持的不匹配；代码和契约都不应被自动视为正确。不要因为契约在同一次更改中被弱化或删除，就忽略违规。区分有意且一致的规范更改与隐蔽回归。
4. 对于每个新增、更改或明确指定的契约，检查其实现声明和使用方，包括未更改的调用方；同时遵循上述相关性规则。使用 rg 和源代码导航查找调用方和引用。追踪导入、重新导出、别名、包装器以及类型／成员的使用；确认每个匹配项都指向受影响的声明。对于目录契约，检查其子树中的相关代码以及受影响声明的使用方。
5. 在每个检查过的调用方／引用处，使用 cc-check list <caller-location> 或手动检查，找出其自身适用的契约。检查调用是否遵守被调用方的契约，以及被调用方更改后的保证是否仍使调用方符合自身契约。沿包装器追踪证据；不要假定使用方兼容。
6. 每个受影响声明最多检查 64 个不同的调用方／引用，并对重叠的调用方和引用去重。优先检查已更改的调用方、高风险行为和多样化的使用模式。这也限制了通过调用方进一步调查的范围。在分析过程中记录调用方数量、未检查范围、搜索限制和不确定的关联关系。如有限制会实质影响结论，请在相关发现中说明。若检查数量受限或受阻，绝不要暗示已完成穷尽验证。

复用针对所检查版本已适用的验证结果。遵守沙箱限制；仅仅工具不可用或运行失败，并不能证明存在契约违规。继续分析源代码，并报告实质性的验证限制。

如果调用方工作流指定了输出格式，请遵循该格式。否则，请简洁地报告发现，并注明契约 ID 和声明／文件、精确源位置、证据及后果。如果发现是既有违规，请明确指出；避免推测性或无关的常规审查结论。如果未发现违规，请说明所检查范围内未发现违规，并列出任何实质性限制。