参考文档 / ZLIB × LEAN
内存、翻译与外部输入输出语义
此页源文件快照 ·
00a7fbc60cc0c90b · 对应提交的原文 ↗本项目证明关于 C 的可执行 Lean 翻译的命题。本节解释翻译表示什么、规范怎样描述它，以及与 C 的哪些联系仍依赖审阅。这里不记录进度；相关记录统一在进度中。
先读架构，再按问题查阅：
| 问题 | 文档 |
|---|---|
| C、运行时、规范与证明怎样组合？ | 架构 |
| 一个 C 语句必须怎样翻译？ | 翻译规则 |
| 不涉及堆的 API 关系描述什么？ | API 模型与具体实现边界 |
| 内部辅助函数的前置条件在哪里定义？ | 内部调用规范 |
| 外部世界表示哪些文件、格式化和错误行为？ | 外部 I/O |
| 有哪些记录和指针种类？ | 生成的运行时结构参考 |
API 手册描述公开调用，证明指南解释怎样建立它们的性质，检查指南解释结果怎样验收。判断任何定理的适用范围时，请同时阅读安全性、可信基础和表示限制。