Typeof.net

指针的 Hoare Logic:Separation Logic

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

{brace: P :brace ~ e~ brace: Q :brace quad brace: Q :brace ~ f ~ brace: R :brace} over {brace: P :brace ~ e; f ~ brace: R :brace} ~~ ("sequent"){{P}e{Q}{Q}f{R}/{P}e;f{R}}(sequent)

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

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

  1. 断言 emp bfemp 表示堆的定义域是空的。
  2. 算符 mapsto 表示指针指向,即若 s,h models e mapsto fs,hef 当且仅当 "dom" ~ h = brace: e :brace wedge h(e) = fdomh={e}h(e)=f
  3. 算符 * 叫做分离合取,若状态 (s, h)(s,h) 满足 P * QPQ,则 hh 一定可以拆分成正交的两个部分 j, kj,k 使得 (s, j)(s,j) 满足 PP 同时 (s, k)(s,k) 满足 QQ
  4. 算符 -* 称为「法杖」或者分离蕴含,若状态 s,h models P -* Qs,hPQ,那么就表示对所有和 hh 正交且满足 PP 的堆 jj,有 s,(h cup j) models Qs,(hj)Q

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

{s, h models P * (P -* Q)} over {s, h models Q}{s,hP(PQ)/s,hQ}

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

x mapsto 3,y wedge y mapsto 3,xx3,yy3,x 则是:

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

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

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

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

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

分配内存 e = new mathfn(v) e=new(v) 的规则稍有些复杂:brace:{e = v' wedge emp bf}:brace ~ e = new mathfn(v) ~ brace:{e mapsto v}:brace{e=v{}emp}e=new(v){ev}(其中 v'v{}ee 彼此不同)。Separation Logic 不允许分配内存之后不初始化,所以 new mathfnnew 总是带有初始值。

最后一条推理规则是针对解引用 e = * nospace f e=f 的:brace:{e=v' wedge f mapsto v}:brace ~ e = * nospace f ~ brace:{e=v wedge f mapsto v}:brace{e=v{}fv}e=f{e=vfv}v, v', ev,v{},e 彼此不同)。

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