逻辑层语法

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、struct_namestruct_name、fieldfield）与类型缩写 addraddr、bytebyte，整数字面量后缀 ii，分离逻辑连接词，以及一套将逻辑变量与程序变量关联起来的命名约定。

本组参考页面涵盖这两部分：HOL Light 已有的语法，以及 C* 增加的内容。

HOL Light 语法说明从 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），以及用于在程序中引入引用的 cst::cst:: 属性一览。