指针的 Hoare Logic:Separation Logic

Hoare Logic 是证明程序正确性的法宝,具体而言,它给出了逐步推理程序正确性的方法。Hoare Logic 使用符号 {P}e{R} 表示程序步骤 e 执行前后的行为:若断言 P 在执行前成立,则 e 执行后断言 R 成立。一些推理规则是很显而易见的:比如

{{P}e{Q}{Q}f{R}/{P}e;f{R}}(sequent)

Hoare Logic 推出后在程序正确性证明方面成为了利器,然而它有一点没有包含,就是没有处理指针,于是 John C. Reynolds 等扩展的 Separation Logic 很好地处理了指针相关的内容。

Separation Logic 中的程序状态分为两个部分:栈区 s 和堆区 h,堆 h 定义为地址到值的函数。两个堆正交若且唯若其定义域不交,记作 h{1}h{2}。Separation Logic 定义了四个附加的断言符号来声明堆的性质:

  1. 断言 emp 表示堆的定义域是空的。
  2. 算符 表示指针指向,即若 s,hef 当且仅当 domh={e}h(e)=f
  3. 算符 叫做分离合取,若状态 (s,h) 满足 PQ,则 h 一定可以拆分成正交的两个部分 j,k 使得 (s,j) 满足 P 同时 (s,k) 满足 Q
  4. 算符 称为「法杖」或者分离蕴含,若状态 s,hPQ,那么就表示对所有和 h 正交且满足 P 的堆 j,有 s,(hj)Q

分离合取和分离蕴含与逻辑学中的合取蕴含极其相似(例如,分离蕴含的前件为假时也成立),例如,Separation Logic 也可以定义一条肯定前件出来:

{s,hP(PQ)/s,hQ}

在这四个算符的基础上 Reynolds 等还定义了其他的符号,如对定义域没有要求的箭头 (表示「内存中有一项……」而非「只有一项」)和指向连续内存的记号 ef{1},f{2},...,f{n} 等。下图表示了 x3,yy3,x 对应的内存情形:

x3,yy3,x 则是:

因为被 连接的两条子断言描述的是同一片内存。

Separation Logic 用于证明程序正确性的方式和 Hoare Logic 相似,但是有额外的 5 条推理规则。

首先是「框法则」,一个「好」程序不应该干涉和它不相关的内容,换言之如果程序满足 {P}e{Q},那么对于任意的内存断言 R,若 R 中没有被 e 指向的目标,则一定有 {PR}e{QR}

对指针赋值 e=f 而言,Separation Logic 定义了公理 {ex}e=f{ef},这个公理实际上明确了很多东西:除了被指向的目标外,还要求指针 e 已经被分配了内存,野指针就是被这么消灭的。

解分配 disposee 的规则也很明确:{ex}disposee{emp},一个(只有 e 的)堆被释放内存之后,它就空啦!

分配内存 e=new(v) 的规则稍有些复杂:{e=vemp}e=new(v){ev}(其中 ve 彼此不同)。Separation Logic 不允许分配内存之后不初始化,所以 new 总是带有初始值。

最后一条推理规则是针对解引用 e=f 的:{e=vfv}e=f{e=vfv}v,v,e 彼此不同)。

在 Separation Logic 推出之后许多人(包括发明者 Reynolds 等在内)都对其进行了各种扩展,比如针对并行的(各位可想想互相独立的并行进程 p||q 的推理规则怎么写),处理垃圾收集的,等等。