概览

教程通过一个个程序来讲授 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* 工具链 开始，沿着教程一直读到对一个已验证函数的结构感到熟悉为止，等到需要教程略去的细节时再回到这里。