指针的 Hoare Logic:Separation Logic
Hoare Logic 是证明程序正确性的法宝,具体而言,它给出了逐步推理程序正确性的方法。Hoare Logic 使用符号 {P} e {R} 表示程序步骤 e 执行前后的行为:若断言 P 在执行前成立,则 e 执行后断言 R 成立。一些推理规则是很显而易见的:比如
Hoare Logic 推出后在程序正确性证明方面成为了利器,然而它有一点没有包含,就是没有处理指针,于是 John C. Reynolds 等扩展的 Separation Logic 很好地处理了指针相关的内容。
Separation Logic 中的程序状态分为两个部分:栈区 s 和堆区 h,堆 h 定义为地址到值的函数。两个堆正交若且唯若其定义域不交,记作 h{1}⊥h{2}。Separation Logic 定义了四个附加的断言符号来声明堆的性质:
- 断言 emp 表示堆的定义域是空的。
- 算符 ↦ 表示指针指向,即若 s
, h ⊧ e ↦ f 当且仅当 dom h = {e} ∧ h(e) = f。 - 算符 ∗ 叫做分离合取,若状态 (s
, h) 满足 P ∗ Q,则 h 一定可以拆分成正交的两个部分 j, k 使得 (s, j) 满足 P 同时 (s, k) 满足 Q。 - 算符 −∗ 称为「法杖」或者分离蕴含,若状态 s
, h ⊧ P −∗ Q,那么就表示对所有和 h 正交且满足 P 的堆 j,有 s, (h ∪ j) ⊧ Q。
分离合取和分离蕴含与逻辑学中的合取蕴含极其相似(例如,分离蕴含的前件为假时也成立),例如,Separation Logic 也可以定义一条肯定前件出来:
在这四个算符的基础上 Reynolds 等还定义了其他的符号,如对定义域没有要求的箭头 ↪(表示「内存中有一项……」而非「只有一项」)和指向连续内存的记号 e ↦ f{1}
而 x ↦ 3
因为被 ∧ 连接的两条子断言描述的是同一片内存。
Separation Logic 用于证明程序正确性的方式和 Hoare Logic 相似,但是有额外的 5 条推理规则。
首先是「框法则」,一个「好」程序不应该干涉和它不相关的内容,换言之如果程序满足 {P} e {Q},那么对于任意的内存断言 R,若 R 中没有被 e 指向的目标,则一定有 {P ∗ R} e {Q ∗ R}。
对指针赋值 ∗e = f 而言,Separation Logic 定义了公理 {e ↦ x} ∗e = f {e ↦ f},这个公理实际上明确了很多东西:除了被指向的目标外,还要求指针 e 已经被分配了内存,野指针就是被这么消灭的。
解分配 dispose e 的规则也很明确:{e ↦ x} dispose e {emp},一个(只有 e 的)堆被释放内存之后,它就空啦!
分配内存 e = new(v) 的规则稍有些复杂:{e = v′ ∧ emp} e = new(v) {e ↦ v}(其中 v′ 和 e 彼此不同)。Separation Logic 不允许分配内存之后不初始化,所以 new 总是带有初始值。
最后一条推理规则是针对解引用 e = ∗f 的:{e = v′ ∧ f ↦ v} e = ∗f {e = v ∧ f ↦ v}(v
在 Separation Logic 推出之后许多人(包括发明者 Reynolds 等在内)都对其进行了各种扩展,比如针对并行的(各位可想想互相独立的并行进程 p || q 的推理规则怎么写),处理垃圾收集的,等等。