分离逻辑

EN | 中文

C* 的断言就是分离逻辑断言，而 C* 中的分离逻辑并非由黑盒求解器支撑的一套固定记号，而是 HOL Light 内部的一次浅嵌入（shallow embedding），分三层构建；本部分对每一层的规定都与证明内核中的实际实现一致。

最底层是具体内存模型。内存是从地址到内存单元的全函数 mem = addr -> mem_varmem = addr -> mem_var，其中每个单元处于三种状态之一：无权限、已分配但未初始化、已初始化并存有一个字节。地址与字节都是整数，因此该模型以字节为粒度，地址运算即整数运算。内存的拆分由三元关系 mem_join m1 m2 mmem_join m1 m2 m 表达，而不借助偏运算。

中间层是断言语言。一条断言就是一个关于内存的谓词：hprophprop 是 :mem->bool:mem->bool 的缩写。每个连接词——****、-*-*、&&&&、||||、-->-->、existsexists、forallforall、empemp、purepure、factfact、truetrue、falsefalse——都是一条 HOL 定义，其定义体是模型之上的一个 lambda 子句；蕴含 |--|-- 展开之后，就是在全体内存上逐点成立的蕴涵。这一层没有任何东西是公理化引入的，因此你能写出的任何断言都不会扩大可信基础。

最上层是规则集——**** 的结合性与交换性、empemp 作为单位元、魔术棒的伴随关系、框架规则、纯事实规则与量词规则。每一条规则都是从内存模型与各连接词的定义中证明出来的；这一层没有任何东西是公理化引入的。叠加在裸字节之上的带类型内存谓词同样是证得的；定义它们的那一页记录的，是理论在复合 C 类型上保持沉默之处。

本部分内容

内存模型与断言——地址、字节与三状态单元；内存及其合并关系；hprophprop 与各连接词的定义；蕴含与等价；purepure 与 factfact 的区别；迭代分离合取；记号汇总。
证明规则——规则目录，其中每一条都是已证明的定理：蕴含、**** 的代数性质、框架消除、各条伴随关系、命题规则与量词规则，以及在 C* 证明中如何把一条规则取为 thmthm。
带类型的内存谓词——data_atdata_at、undef_data_atundef_data_at、array_atarray_at 及其同族谓词如何叠加在字节单元之上、它们内建的有效性与范围约束，以及对它们进行拆分、合并与换基的规则。