概览

教程通过一个个程序讲解 C*，每次只引入一个概念，让每一步都由前一步自然引出。那些会打断讲解主线的细节，则留到后面再讨论。

参考手册的组织方式不同：它直接陈述事实，方便读者按需查找，而不以顺序阅读为目标，并假定读者已经知道自己要查什么。每一页都可供直接查阅，无须跟随逐步展开的论证。你需要确认反引号内允许使用的准确语法、即将使用的某条规则的准确表述，或证明块所调用函数的准确 C 签名，就可以来这里查阅。

C* 源文件混合了三种语言。查阅参考手册时，大多数问题都与当前正在使用哪一种语言有关。确定所处的层次，通常就能找到该查阅的页面。

逻辑层包括反引号之间的全部内容：[[cst::require(...)]][[cst::require(...)]]、[[cst::ensure(...)]][[cst::ensure(...)]] 与 [[cst::invariant(...)]][[cst::invariant(...)]] 中的断言，以及传给证明函数的项。这些文本不是 C 代码，由 HOL Light 的项解析器解析，支持的常量与记号也经过扩展，加入了 C* 专有的部分。这一层涉及词法与文法问题：哪些标识符是保留字、某个运算符的结合性如何、0i0i 中的 ii 是什么含义、某个常量是什么类型。这些问题可查阅逻辑层语法。

断言层关心这些项的含义。一条良构的断言表示一个关于内存的谓词，针对它的证明步骤须遵循分离逻辑的规则：哪些状态满足 data_at p Tint vdata_at p Tint v、**** 对它所连接的两部分各有什么要求、哪条规则允许丢弃一个合取项，以及某条规则是原始定律还是由原始定律得出的推论。这些问题可查阅分离逻辑。

实现层就是普通的 C。证明块是需要编译的 C 代码，其中的操作，包括构造项、应用推理规则、读取符号状态、卸除验证条件，都是通过函数调用完成的。这些函数声明在随工具链发布的头文件中。这一层涉及 C API 的常规问题：签名是什么、返回什么、失败时如何处理。这些问题可查阅内核头文件。

如果你还没有安装工具链，或还没有写过 C* 文件，请先从安装 C* 工具链开始阅读教程。等到熟悉了已验证函数的结构，需要查阅教程略去的细节时，再回到参考手册。