1. 一次完整的压缩与解压任务

总览 · 下一章：字节如何变成编码

应用保存八个字节 ABABABAB，稍后再还原它们。 沿着这项任务，可以把调用者的字节、库的输出和所用资源联系起来。 这里的一项“任务”包括建立状态、处理字节和释放内部资源；一次函数返回只是其中一步。后面分别说明应用已交出的输入、库已交付的输出，以及仍由流保管的资源。 下文按共同的范围与证明方法解释实现行为。完整执行证明未完成，仍需把实际消费的输入、交付的输出和资源清理逐项连接起来。

目录

• 1.1 跟随八个字节
• 1.2 建立、处理与释放
• 成功路径
• 失败与放弃任务
• 1.3 已消费输入与已交付输出
• 1.4 空间不足或数据损坏
• 1.5 将两个引擎分别连接到字节含义

1.1 跟随八个字节

这些字节的十六进制值是 41 42 41 42 41 42 41 42。 zlib 将它们当作字节处理，图像数据、序列化记录或内嵌的零也一样。

中间一行是一种有效的 zlib 格式编码，并不承诺不同版本、配置或调用安排都会输出相同字节。 编码与格式包装两章会解释主体、头部和尾部。

十二个字节表示八个字节：编码和包装的开销可能超过节省的空间。 因此，输出容量需要经过证明的上界。同一份输入可以有多种表示；正确性依照独立的 格式关系判断，而不是要求输出等于某个指定的压缩字节串。

这个例子选用默认 zlib 包装，不使用预置字典，并采用通常的校验行为。 更广的定义域仍由输入配置规范规定。

1.2 建立、处理与释放

成功路径

用 deflateInit 和 Z_DEFAULT_COMPRESSION 创建压缩器。 提供缓冲区并调用 deflate；全部输入已经提供后，请求 Z_FINISH。 Z_STREAM_END 表示完成，deflateEnd 释放内部资源。

解压是一项独立任务：用 inflateInit 创建解压器，提供编码后的字节， 调用 inflate 直至完成，再用 inflateEnd 释放资源。 初始化只准备状态，不执行压缩或解压。这里的状态记录处理进度和内部存储位置；调用者的原始字节仍放在调用者提供的缓冲区。 精确的调用条件见压缩与 解压契约。

两个引擎不必属于同一个程序：生产者可以今天写出数据，另一位使用者日后再解码。 格式是双方共同遵守的约定。

失败与放弃任务

初始化失败时，必须撤销本次尝试中完成的每次分配。 初始化成功后，流拥有内部资源，直到调用结束函数：压缩用 deflateEnd，解压用 inflateEnd。下文把这类释放操作统称为 End。

flowchart TD
    fresh["调用者拥有流记录与缓冲区"] --> init["初始化引擎"]
    init -->|"成功：取得内部资源"| live["引擎存活"]
    init -->|"失败：撤销本次分配"| none["本次未留下内部资源"]
    live -->|"继续处理数据"| live
    live -->|"完成"| complete["处理完成，仍拥有内部资源"]
    live -->|"放弃或处理错误：释放资源"| released["内部资源已释放"]
    complete -->|"结束函数"| released

图中表示任务期间的所有权变化，并未列举全部 API 转移。 调用者始终保有自己的记录与缓冲区。

应用可以在出错后，或不再需要数据时放弃解压。 End 释放资源，不再处理剩余数据。 对压缩而言，End 还会丢弃待输出内容。 即使内部存储已经释放，它仍可能报告任务被提前放弃；详见 结束契约。

所以，仅仅还原八个字节还不能建立整个生命周期的性质。 初始化建立所有权，各次调用保持所有权，End 将每个拥有的分配恰好释放一次。 共同的证明方法解释如何组合这些步骤。

1.3 已消费输入与已交付输出

一次调用可能只消费所提供的 ABABABAB 中的 ABA。 剩余 BABAB 必须再次提供。 更新后的输入指针和计数确定已消费的字节，输出指针和计数确定已写入的字节。

压缩器可以在内部保留未完成的工作，因此同一次调用的输入消费量和输出交付量不必对应。 流式处理一章会跟踪缓冲区边界与保存的状态。

证明记录累计已消费输入和已交付的编码前缀。 完成之前，这个前缀不必已经构成完整、可解码的数据流，但必须与保留的状态对应。 结束处理完成后，整个编码必须恰好表示 ABABABAB。

1.4 空间不足或数据损坏

如果解压器只有七个输出位置，第八个解码字节就必须等待更多空间，不能写出所给范围。 流式处理解释怎样继续。

输出可能早于尾部错误被交付。格式包装解释为什么已有输出不能证明整个流已通过校验。

格式错误的数据仍在安全性定义域内。无效指针则受另一组调用者义务约束； 期待错误返回并不能使无效指针安全。详见 有定义的拒绝与内存义务。

整个任务要完成，必须持续有足够的输入、输出机会，并发出所需的结束请求。 重复无进展的请求不能保证完成。 每次调用的终止证明还须单独排除循环步数预算耗尽。

1.5 将两个引擎分别连接到字节含义

只把往返还原作为正确性标准并不充分：两个引擎可能彼此一致，却都违背可互操作的格式。

flowchart LR
    original["原始字节：ABABABAB"] --> compressor["实际压缩器执行"]
    compressor --> encoded["写出的字节"]
    encoded --> decoder["实际解压器执行"]
    decoder --> recovered["还原字节：ABABABAB"]
    format["独立定义的格式含义"] -->|"编码表示原始输入"| encoded
    format -->|"解码符合所表示的字节"| recovered

上方路径执行实际任务，下方两条联系分别把翻译后的实际缓冲区和执行连接到字节含义。 一个已经假定期望行为的模型不能建立其中任何一条联系。

压缩器论证跟踪已消费输入如何经过符号、位和已交付字节； 解压器论证跟踪输入位如何经过表解释和历史复制进入输出。 技术细节见压缩器与解压器证明指南。 辅助函数的前提必须由初始化和之前的执行推出。

共同的验收规则涵盖安全性、资源和证据。 有限例子测试可以发现不一致，但不能证明全称命题。

继续阅读字节如何变成编码，查看编码内部的机制及各自需要的不变量。