参考文档 / ZLIB × LEAN

契约的结构与范围

此页源文件快照 · 67c5819862b2b917 · 对应提交的原文 ↗

契约回答三个问题：调用者必须提供什么、返回时调用者能依赖什么、调用期间什么可以改变？阅读单个条目前，先读页面的公共规则。它们给出内存、生命周期和构建假设，避免在每个函数下重复。

条目结构

部分	含义
C 签名	函数的 C 名称和参数类型，保留声明宏。
用途	调用者想执行的操作。
定义域	本契约覆盖哪些值、对象和调用历史。
前置条件	调用前要求的条件，包括经过检查的拒绝情况。
后置条件	各条所述返回路径的结果和保证。
允许的影响	读取、写入、分配、释放、文件操作和借用存储。
边界情况或错误	空输入、部分输出和拒绝等会改变结果使用方式的情况。

错误返回通常不会撤销已经完成的工作。输出、指针推进、长度单元或文件位置可能已经改变。应遵循所述返回路径及其影响。尤其是，解码中的分配失败可能发生在部分输出之后。

定义域与影响彼此独立

受限定义域要求的不只是参数类型中的值。指针通常必须指向仍有效的存储；句柄需要合法调用历史；校验和组合可能要求使用为正确长度生成的算子。

完整类型定义域覆盖所选构建中参数类型的每个值，包括规定的拒绝。即使函数覆盖每个标量值，它的整体定义域仍可能受限，因为它的指针必须指向有效存储。这里区分的不是有限与无限，也不是有界与无界。

影响	含义
纯计算	不读取调用者内存、不改变状态，只计算结果。可以使用固定的库常量或表。
只读	读取调用者内存或流状态并保持其不变。借用的返回结果仍归库所有。
有状态	可以写入调用者目标或库状态、分配或释放存储、调用回调，或执行文件 I/O。

这些标签描述不同性质。纯计算也可以有受限定义域。查询即使不改变流，只要写入可选标量结果，就仍有写入影响。

示例：组合两个 CRC

crc32_combine_op 避免重新读取原始字符串。设 A 为前一段字节，B 为后一段字节。crc1、crc2 分别保存两段独立算出的 CRC；op 则表示“把前一段的 CRC 向后推进 B 的字节长度”所需的运算。例如 B 有 100 字节，便必须使用为长度 100 生成的算子，而不能使用为长度 99 生成的算子。

下面把这个要求写成一份简短契约：

定义域：受限定义域。
前置条件：crc1 是 A 的 CRC；crc2 是 B 的 CRC；
          op 是根据 B 的可表示非负长度生成的算子。
后置条件：结果是 A 后接 B 的 CRC。
允许的影响：纯计算。

A 的 CRC 指以零为起始值对 A 调用 crc32。A 和 B 是普通字节序列，不需要特殊的 CRC 类型。即使调用不读取调用者内存，生成的算子和正确长度仍然重要。零长度和负长度情况见校验和条目，与标准的一致性见格式模型。

共享阅读规则

除非条目另有说明，使用默认 LP64 Linux 静态构建和默认分配器。在整个调用期间，可读、可写范围都必须包含所述字节数。长度须能由参数类型表示。有效句柄已经初始化、尚未关闭，按顺序使用，且调用者不修改其拥有的状态。

在前置条件成立时，契约要求执行终止且不发生未定义行为，满足后置条件，并且只改变所述作用范围。分配失败、部分结果和清理也是这一要求的一部分。共享流规则解释公共所有权和帧性质义务；安全定义模型中的故障。

这些是聚焦于特定范围的文档契约。更窄的前置条件既不改变已登记的 Lean 目标，也不让被排除的调用变成未定义行为。参见范围偏差和已登记公开目标。证明状态和剩余工作只记录在进度中。