算法精读与形式化验证

一次压缩任务，从调用者提供的字节开始。窗口与匹配生成符号，编码器把符号写成比特，解码器沿相反方向恢复字节；缓冲区可能在任意一次调用后更换，分配也可能失败。

证明沿着这些实际对象前进：先精读一个组件的算法、布局和优化，再说明它需要建立的关系，以及关系怎样交给下一个组件。每个主题的最后一章集中讲证明思路，可以与前面的算法互相跳转。