分离逻辑

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 子句；蕴含 |--|-- 展开之后，就是在全体内存上逐点成立的蕴涵。这一层没有任何东西是公理化引入的，因此你能写出的任何断言都不会扩大可信基础。

最上层是规则集。四条分离代数定律（unit_joinunit_join、unit_specunit_spec、join_commjoin_comm、join_assocjoin_assoc）是从内存模型中证明出来的；其余每一条定律——**** 的结合性与交换性、empemp 作为单位元、魔术棒的伴随关系、框架规则、纯事实规则与量词规则——都由这四条定律连同各连接词的定义派生而来。只有叠加在裸字节之上的带类型内存谓词才会引入公理，而这些公理在出现之处都逐条标注。

本部分内容

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