Hoare Logic

程序正确性

直觉上,要证明一个程序的正确性,就需要表达什么是正确性。举个例子,你要八岁的孩子去打酱油,把打酱油当成一条计算机指令,而当孩子成功打回酱油时,就说明你要的要求已经达到。因此,一个程序给出后,我们需要描述我们的要求,然后证明程序满足了我们的要求。

1
2
3
4
5
6
7
8
9
float sum(float *array, int length) {
float sum = 0.0;
int i = 0;
while (i < length) {
sum = sum + array[i];
i = i + 1;
}
return sum;
}

$a + y $

历史

Hoare Logic是用来分析程序正确性的,其想法就是提供一套机制,用以描述程序和用户之间的协议。

Hoare Logic在六十年代由Tony Hoare提出来Hoare67, Folyd 在早年也发表了类似的想法。

Hoare Logic

1. 霍尔元组 Hoare Triple

Hoare Logic用霍尔三元组Hoare Triple来描述程序的正确性。一个Hoare Triple定义如下:

\\\{P\\\} C \\\{ Q\\\}

其中PPQQ都是断言assertion,用谓词逻辑predicate logic表示,C是程序语言的一条指令。PP通常被称为前置条件precondition,而QQ被称为后置条件postcondition

这个Hoare Triple \\{P\\} C\\{ Q \\} 表达的是,当程序从某个状态 ss 开始执行 CC,并且 PPss 状态下成立(值为真True),当 CC 执行并终止时,程序到达一个新的状态 ss',在这个状态中,QQ 成立。

直白一点说,程序执行之前,前置条件必须成立,程序执行指令之后,定义的后置条件必须满足。

{前置条件:小彬八岁}
指令:去楼下小卖部打酱油
{后置条件:家里有了酱油}

然而,上述Hoare triple的正确性是有条件的。因为我们假设了指令一定会终止,比如,我们假设了小彬一定会把酱油带回家,而事实上,小彬可能没回家,打酱油的指令一只在未确认状态,所有后置条件不会成立。证明指令会不会终止是个经典的不可判断问题。若不要求指令一定会终止,其则是partially correct,若指令一定会终止,则为totally correct。


例子: 假设有Hoare triple:

\\\{x == 5\\\} x:=x*2\\\{x>0\\\}

假设在执行赋值语句 x:=x2x:=x * 2 前,xx 的取值为5,因此前置条件满足。执行 x:=x2x:= x * 2 后,xx 的值更新为10。因为 x=10 \\Rightarrow x > 0,因此该Hoare triple是正确的。

但是,我们描写的后置条件 x>0x>0 并不是完美的,因为如果 x=30x=30,后置条件依然满足,但是其实这并不是程序真正执行后的结果。因此,我们需要修改后置条件(write a stronger postcondition)。

2. 最强后置条件 Strongest Postconditions

上述例子中,我们写了很多后置条件,如下:

  • \\\{x == 5\\\} x:=x*2\\\{True\\\}
  • \\\{x == 5\\\} x:=x*2\\\{x>0\\\}
  • \\\{x == 5\\\} x:=x*2\\\{x=10 \\lor x =5 \\\}
  • \\\{x == 5\\\} x:=x*2\\\{x=10\\\}

这些triple全部都是正确的,但是哪个后置条件才是最强的呢?


定义:最强后置条件 Strongest Postconditions
如果有元组 \\{P\\} C\\{ Q \\} 和后置条件集合 KK,对于任意的一个后置条件 p \\in K,如果 \\{P\\} C\\{ p \\} 正确,并且 $ Q \Rightarrow p$,我们就称 QQ 为指令 CC 在前置条件 PP 下的最强后置条件。上述例子中,我们有

  • $ x = 10 \Rightarrow True$
  • $ x = 10 \Rightarrow x>0 $

因此,该例子中,x=10x = 10 为最强后置条件。


3. 最弱前置条件 Weakest Preconditions

同样的,对于给定的后置条件 QQ 和指令 CC,我们可以计算 Hoare triple需要的最弱前置条件。


定义:最弱前置条件 Weakest Preconditions
假如有元组\\{P\\} C\\{ Q \\} 和前置条件集合 MM,假如 KK 所有的前置条件 k \\in K, k \\Rightarrow P,则 PP 则是对于指令 CC 和 后置条件 QQ 的最弱前置条件,通常用 wp(C,Q)wp(C,Q)表示。


最弱前置条件是可以计算的。对于不同的程序语句,计算最弱前置条件定义如下:

  • $ wp(x:=e, Q) = [e/x]Q$
  • $ wp(s_1;s_2, Q)= wp(s_1, wp(s_2,Q))$
  • $ wp ($ if BB then s1)s_1) else s_2, Q) = B \\Rightarrow wp(s_1, Q) \\land (\\neg \\Rightarrow wp(s_2, Q))

当涉及到循环时,往往我们需要知道变量先前的值 old value 和当前的值,然后进行比较。另外一种做法是,不管循环怎么执行,总有一个不变式invariant II,程序在循环中执行到任何状态都是满足的。因此我们只要给循环定义一个不变式 II,就可以研究循环程序的正确性。

定义:给定循环程序\\{ P \\}while BB do CC done \\{ Q\\} 和不变式 II, 程序如果正确,当且以下条件成立:

  • $P\Rightarrow I $: 前置条件满足不变式 ;
  • \\{ I \\land B\\} C \\{I\\}: 每一次执行,不变式保持;
  • \\{I \\land \\neg B \\Rightarrow Q \\}: 程序跳出循环时,后置条件满足。