Skip to main content

06 Hoare Logic

这篇笔记介绍lecture11，Hoare Logic的内容。

基本概念​

霍尔三元组​

程序状态包括程序中所有使用变量的值。前置条件描述执行程序前的程序状态，后置条件描述执行程序后的程序状态。前置/后置条件可以是谓词逻辑公式。

如果程序C在初始满足前置状态的条件中执行，并且如果C的执行终止，则C的终止状态满足后置条件，那么程序C是部分正确的（注意，部分正确性不考虑程序是否可以终止）。可以用霍尔三元组来定义程序正确性。

霍尔三元组可以写作 {P} C {Q}\{P\}~C~\{Q\} ，其中 {P}\{P\} 是前置条件， CC 是程序， {Q}\{Q\} 是后置条件。例如， {x=1} x=x+1 {x=2}\{x = 1\}~x = x + 1~\{x = 2\} 是部分正确的。

停机问题​

停机问题指，是否存在一个算法可以给出任意程序是否会停止（基本上停止意味着终止）。

事实上没有通用算法可以解答停机问题。

命令式语言​

简单起见，不考虑那些包含指针、函数、结构体、堆栈等待的程序。

那么命令式语言有以下几种：

  • skip ：什么都不做
  • a := e ：赋值，将 e 的值赋值给 a
  • s1; s2 ：顺序执行 s1 和 s2
  • if(b) {s1} else {s2} ：如果 b 为真执行 s1 ，否则执行 s2
  • while(b) {s} ：在 b 为真时重复执行 s

霍尔逻辑与程序验证​

公理​

对于任何 {P}\{P\} ，都可以得出 {P} skip {P}\{P\}~skip~\{P\} 一定为真。

赋值语句的处理更为复杂。

对于 {P}a:=e\{P\}a:=e ，可能会认为 {P}a:=e{P[a/e]}\{P\}a:=e\{P[a/e]\} （ {P[a/e]}\{P[a/e]\} 指用 aa 代替 PP 中的 ee）和 {P}a:=e{P∧a=e}\{P\}a:=e\{P\land a=e\} 这两个公式为真。但是这两种公式都不是永真的。对于前者，有反例 {a=0}a:=1{a=0}\{a=0\}a:=1\{a=0\} ；对于后者，有反例 {a=5}a:=a+1{a=5∧a=a+1}\{a=5\}a:=a+1\{a=5\land a=a+1\} 。

第一种正确的公式是 {P}a:=e{(∃v)(a=e[v/a]∧P[v/a])}\{P\}a:=e\{(\exists v)(a=e[v/a]\land P[v/a])\} （为真）。例如，对于 {a=1}a:=a+1\{a=1\}a:=a+1 ，有 {a=1}a:=a+1{(∃v)(a=v+1∧v=1)}\{a=1\}a:=a+1\{(\exists v)(a=v+1\land v=1)\} ，即 {a=1}a:=a+1{a=2}\{a=1\}a:=a+1\{a=2\} ，显然为真。

此外，还有一种正确的“backward”公式， {P[e/a]}a:=e{P}\{P[e/a]\}a:=e\{P\} （为真）。例如，{a−b>3}a:=a−b{a>3}\{a-b>3\}a:=a-b\{a>3\} 为真。

上面两种公式，第一种的简称是AS-FW，第二种的简称是AS。AS的应用比AS-FW更广泛，因为它不涉及量词。

推理规则​

除了AS-FW与AS外，还有其它推理规则。

如果 P→QP \rightarrow Q ，则认为 PP 是强的， QQ 是弱的。如果有 {P} C {Q}\{P\}~C~\{Q\} 和 Q→RQ \rightarrow R ，则有 {P} C {R}\{P\}~C~\{R\} ，为WC（weakening consequence）规则，写作

{P} C {Q}  Q→R{P} C {R}\frac{\{P\}~C~\{Q\}~~Q\rightarrow R}{\{P\}~C~\{R\}}

注意

AB\frac{A}{B}

代表 A  ⟹  BA \implies B 。

类似地，有SP（strengthen precedent）规则

P→Q  {Q} C {R}{P} C {R}\frac{P\rightarrow Q~~\{Q\}~C~\{R\}}{\{P\}~C~\{R\}}

以上的规则都只适用于单个的语句。

对于顺序结构，有SC规则（顺序组合规则，sequential composition rule）

{P} C1 {R}  {R} C2 {Q}{P} C1;C2 {Q}\frac{\{P\}~C_1~\{R\}~~\{R\}~C_2~\{Q\}}{\{P\}~C_1;C_2~\{Q\}}

对于条件语句，将条件 b 化为命题后，有CD规则（条件规则，conditional rule）

{P∧istrue(b)} C1 {Q}  {P∧isfalse(b)} C2 {Q}{P}if(b) then C1 else C2 {Q}\frac{\{P\land istrue(b)\}~C_1~\{Q\}~~\{P\land isfalse(b)\}~C_2~\{Q\}}{\{P\}if(b)~then~C_1~else~C_2~\{Q\}}

对于循环，有WHP规则（while规则）

{I∧istrue(b)} C {I}{I}while(b) C {I∧isfalse(b)}\frac{\{I \land istrue(b)\}~C~\{I\}}{\{I\}while(b)~C~\{I \land isfalse(b)\}}

以上这些规则只能验证部分正确性，不能确定程序是否终止。

自动证明​

给定程序 CC 和后置条件 QQ ，如果对于所有 P′P^{\prime} 都有如果 P′→PP^{\prime} \rightarrow P ，那么 {P′} C {Q}\{P^{\prime}\}~C~\{Q\} ，则称 PP 为最弱前置条件，可以将 PP 写为 wp(C,Q)wp(C,Q) 。

类似地，给定程序 CC 和前置条件 PP ，如果对于所有 Q′Q^{\prime} 都有如果 Q→Q′Q \rightarrow Q^{\prime} ，那么 {P} C {Q′}\{P\}~C~\{Q^{\prime}\} ，则称 QQ 为最强后置条件，可以将 QQ 写为 sp(C,P)sp(C,P) 。

对于 {P} C {Q}\{P\}~C~\{Q\} ，如果能找到wp，就可以将原式写为 P→wp(C,Q)P \rightarrow wp(C,Q) ，只需要证明 P∧¬wp(C,Q)P \land \neg wp(C,Q) 不可满足；如果能找到sp，就可以将原式写为 sp(C,P)→Qsp(C,P) \rightarrow Q ，只需要证明 sp(C,P)∧¬Qsp(C,P) \land \neg Q 不可满足。这可以将霍尔三元组转为谓词逻辑，称为谓词变换语义。最后得到的谓词逻辑公式可以用SMT求解。

AS-FW给出最强后置条件，AS给出最弱前置条件；在这里用wlp代替wp，不考虑循环无法终止的情况。对于所有 CC 和 QQ ，都保证 {wlp(C,Q)} C {Q}\{wlp(C,Q)\}~C~\{Q\} 为真；如果 P→wlp(C,Q)P \rightarrow wlp(C,Q) ，就有 {P} C {Q}\{P\}~C~\{Q\} 为真。

最弱前置条件​

现在只需要找出wlp就可以解决这个问题。

对于 skipskip ，显然 wlp(skip,Q)=Qwlp(skip, Q) = Q 。对于赋值语句，通过AS可以知道 wlp(a:=e,P)=P[e/a]wlp(a:=e,P) = P[e/a] 。

进一步，对于顺序语句，有 wlp(C1,C2,Q)=wlp(C1,wlp(C2,Q))wlp(C_1,C_2,Q) = wlp(C_1,wlp(C_2,Q)) ；对于条件语句，有 wlp(if(b) then {C1} else {C2},Q)=(istrue(b)→wlp(C1,Q))∧(isfalse(b)→wlp(C2,Q))wlp(if(b)~then~\{C_1\}~else~\{C_2\},Q)=(istrue(b)\rightarrow wlp(C1,Q))\land (isfalse(b)\rightarrow wlp(C2,Q)) 。

循环更加复杂。对于 {P}while(b)C{Q}\{P\}while(b)C\{Q\} ，要求 P→IP\rightarrow I 、 (I∧isfalse(b1))→Q(I \land isfalse(b1))\rightarrow Q 、 I∧istrue(b) C {I}{I\land istrue(b)}~C~\{I\} 三个式子同时满足。而最后一个式子可以进一步通过wlp证明。

健壮的与完备性​

对于某个验证算法，如果所有通过算法的程序都是正确的，则这个算法是健壮的。注意“正确”有很多种方式定义。先前介绍的所有验证算法都是健壮的。

如果所有正确的程序都可以通过算法，则算法是完备的。先前的所有算法都不是完备的；这些算法可能无法处理无界循环的情况，并且一阶逻辑公式的可满足性问题是不可判定的。