0
0

指针的 Hoare Logic:Separation Logic

Typeof 发表于 1970年01月01日 08:00 | Hits: 1017

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, h ⊧ e ↦ f当且仅当"dom" ~ h = brace: e :brace wedge h(e) = fdom h = {e} ∧ h(e) = f。
  3. 算符*∗叫做分离合取,若状态(s, h)(s, h)满足P * QP ∗ Q,则hh一定可以拆分成正交的两个部分j, kj, k使得(s, j)(s, j)满足PP同时(s, k)(s, k)满足QQ。
  4. 算符-*−∗称为「法杖」或者分离蕴含,若状态s,h models P -* Qs, h ⊧ P −∗ Q,那么就表示对所有和hh正交且满足PP的堆jj,有s,(h cup j) models Qs,(h ∪ j) ⊧ Q。

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

{s, h models P * (P -* Q)} over {s, h models Q}{s, h ⊧ P ∗ (P −∗ Q)/s, h ⊧ Q}

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

而x mapsto 3,y wedge y mapsto 3,xx ↦ 3, y ∧ y ↦ 3, 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{P ∗ R} e {Q ∗ R}。

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

解分配dispose mathfn edispose e的规则也很明确:brace:{ e mapsto x }:brace ~ dispose mathfn e ~ brace: { emp bf } :brace{e ↦ x} dispose e {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) {e ↦ v}(其中v'v{′}和ee彼此不同)。Separation Logic 不允许分配内存之后不初始化,所以new mathfnnew总是带有初始值。

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

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

原文链接: http://typeof.net/2015/m/samasa-02-separation-logic.html

0     0

评价列表(0)