逻辑层语法

C* 源文件包含两种语言。 反引号之外是 C，由 C* 编译器读取。 反引号之内——出现在契约中、全局证明声明中、或传给证明内核函数的实参中——则是逻辑层语言：一个表示 HOL 类型或 HOL 项的逻辑表达式，由 C* 所依托的 HOL Light 证明助手完成词法分析、语法分析与类型检查。

这套内层语言属于 HOL Light，并非 C。 它的词法分析器、优先级表、绑定子与类型推断都是 HOL Light 自带的，因此像 `!n. n > 0i ==> ~(n = 0i)``!n. n > 0i ==> ~(n = 0i)` 这样的项，在 C* 中的含义与在一次 HOL Light 会话中完全相同。 在这一基础之上，C* 增补了面向验证的类型常量（hprophprop、ctypectype、addraddr、bytebyte）、整数字面量后缀 ii、分离逻辑连接词，以及一套把逻辑变量与程序变量关联起来的命名约定。

本组页面是这两半内容的参考：HOL Light 已经提供的部分，以及 C* 增补的部分。

HOL Light 语法 规定所继承的基础：词法结构（字符类别、标识符、保留字、字符串字面量）、类型语法（TyvarTyvar/TyappTyapp 抽象语法、后缀式类型应用、^^、##、++、->-> 构造子及其优先级），以及项语法（VarVar/ConstConst/CombComb/AbsAbs 抽象语法、完整的中缀优先级表、列表与集合概括式、matchmatch 与 letlet 等项的形式、各种绑定子与前缀符，以及类型推断如何解析重载与隐式类型）。

C* 的扩展 规定 C* 在此之上增补的内容：面向验证的类型常量与类型缩写、123i123i 形式的整数字面量、堆命题常量与分离逻辑连接词、带类型的内存谓词、ctypectype 常量以及 sizeofsizeof、min_ofmin_of、max_ofmax_of 与 field_addrfield_addr、定宽位运算符，还有符号执行引擎用来指称程序变量的保留逻辑变量名（x__addrx__addr、x__prex__pre、__return__return）。