| TOP | Code | Math | Luke | Math Book |
Previous: Knight Dialer Next: Drawing Balls from a Bag

简明Hoare Logic

2018-12-08

TDD是工程上最常见的避免写bug的方法，然而TDD只能通过有限个test case覆盖无穷的解空间里若干个离散的点，逻辑证明却能覆盖整个解空间的正确性。 对于证明“简单”程序的正确性，Hoare Logic提供了一种严谨的逻辑方法。 学习Hoare Logic不但可以帮助你写出bug free的代码，还能提高写代码的品味。

针对面试刷题而言，大多数大学算法课以及市面上的算法培训，注重介绍算法和解题的思路，却缺乏对“怎么写代码”的指导。 这导致了很多面试者能提出可行的解题方案，实际动手往往写不出高质量代码，出现低级bug、逻辑混乱、没有考虑边界条件等情况十分常见。 我认为学习Hoare Logic能很大程度缓解这些问题。 无论在刷题练习、白板写题、还是日常工作中，Hoare Logic的思想都是十分受用的。 本文撇去一些严谨的数学定义，着重介绍Hoare Logic的基本规则和思想。

Hoare Logic的核心思路是： 分析比较程序运行前后所满足性质的变化，来验证程序的正确性。 任何一支“简单”的程序，都是由三种基本结构相互嵌套组成的：顺序（sequential）、选择（if-then-else）和循环（while-do）。 如果我们可以找到一些模式，证明在三种基本结构下程序的正确性，也就能证明几乎所有程序的正确性。

Precondition、Postcondition和Skip Rule

Hoare Logic的基本语法由三个部分组成：

  1. 前置条件（Precondition）是程序执行前满足的状态。
  2. 一支“不会死循环”可正确执行的程序。（不提前return、break或者抛出Exception）
  3. 后置条件（Postcondition）是程序执行后满足的状态。

它满足如下格式：P代表Precondition，Q代表Postcondition，S是程序。

{P} S {Q}

其意思是，如果S这支程序执行前满足P这个条件，那么执行后必然满足Q。

首先，我们先看一个最简单的例子：我们的程序只有一行skip语句。 这里的skip相当于Python里面的pass语句，意思是“什么都不做”。 比如程序执行之前x等于3，执行skip之后x依然等于3。我们写成如下式子。

{x = 3} skip; {x = 3}
  • 第一个x = 3是Precondition。
  • 第二个x = 3是Postcondition。
  • 中间的skip;是我们运行的程序。

（注：这里的等号=表示数学上的相等，而不是计算机语言里的赋值，赋值我们后面将用:=表示。）

那么，skip语句的基本规则（我们称之Skip Rule）如下。下式表达的意思，换句话说就是，skip执行前后程序的状态不变。

{P} skip; {P}

Assignment Rule

上面的skip是一支很无趣的程序，接下来我们看看赋值（assignment）语句的例子，比如x := y * 2。 如果程序执行之前满足y等于3，那么执行之后会满足什么条件呢？

{y = 3} x := y * 2; {?}

我想任何一个刚入门的程序员都不难得出结论， 我们可以在Precondition等式两边都乘以2，得到y * 2 = 6，那么根据赋值语句的语义就可以用x替代y * 2的部分得到x = 6。 于是就有了如下式子：

{y = 3} x := y * 2; {x = 6}

（其实，更完整的Postcondition是{x = 6 && y = 3}，因为y没有改变我们就不赘述了。）

这个例子是已知Precondition求Postcondition，再看一个反过来的例子，已知Postcondition求Precondition。 还是同一支程序，如果我们想要程序执行之后满足x小于10，那么程序执行之前，我们需要满足怎样的条件呢？

{?} x := y * 2; {x < 10}

这也非常简单，我们只需要将Postcondition中的x用y * 2替代，就可得到y * 2 < 10，即y < 5。

{y < 5} x := y * 2; {x < 10}

根据上面这个例子，我们将赋值语句的基本规则称为Assignment Rule，记作：

{P[E/x]} x := E {P}

P[E/x]的意思是将P这个式子里面出现的x都用E替代。 在上面的例子里，P是x < 10，E是y * 2，那么P[E/x]就是y * 2 < 10。

再举一个例子，

{?} y := y + 5 {y - 3 > 5}

这里y同时出现在了赋值语句的左右两边，注意E指的是右边y + 5的部分，替代Postcondition内的y，得到(y + 5) - 3 > 5，即y > 3是Precondition。

Consequence Rule

赋值的规则如果光看式子，还是挺绕的，到底是E代替x？还是x代替E？ 其实只要理解了赋值语句的语义，即使不记得具体的替换规则，实际推理的过程也是非常自然的。 接下来，我们来看一条比较显然的规则吧。

经过中学数学证明训练的人，应该都不难发现，我们之前给出的Precondition和Postcontition都是非常“严苛”（tight）的。 拿上面的一个例子的Postcondition说，如果x小于10，那么x显然小于100。 那么，我们是不是也可以有下面这个比较“宽松”（loose）的结果？

{y < 5} x := y * 2; {x < 100}

同理，如果y小于0，那么y必然小于5。 我们又可以得到下面的结论。

{y < 0} x := y * 2; {x < 100}

通过简单的推理转换，我们得到了比较宽松的Precondtion和Postcondition。 我们将这一变换规则称为Consequence Rule，记作：

P => P',  {P'} S {Q'},  Q' => Q
-------------------------------
          {P} S {Q}

这个规则中出现了横线，意思是如果横线上面的三个条件都满足时，那么我们可以得到横线下面的条件。 比如上面的例子就能写成：

y < 0 => y < 5,  {y < 5} x := y * 2; {y < 10},  y < 10 => y < 100
-----------------------------------------------------------------
                {y < 0} x := y * 2; {x < 100}

也就是说，如果一支程序满足一定的Precondition/Postcondition，那么自然满足更加宽松的限制条件。

Sequential Rule

接下来，我们展开对三种基本程序结构（顺序、选择和循环）的讨论。 首先是最朴实的顺序（Sequential）结构。

顺序结构的程序包含了若干条语句，一条接着一条顺序执行。 比如有两条语句S1; S2;，S1执行完了以后执行S2。 那么这样的程序满足Sequential Rule，记作如下式子：

{P} S1 {R},  {R} S2 {Q}
-----------------------
    {P} S1 S2 {Q}

换句话说，顺序程序我们只需要按部就班地推理，前一条语句的Postcondition就是后一条语句的Precondition。 比如下面这支程序，包含两条赋值语句，假设程序执行前满足y小于5。

x := y * 2;
y := x + 3;

我们可以通过下面的推导方法得出：程序执行之后满足x小于10，y小于13。

{y < 5} x := y * 2 {x < 10},  {x < 10} y := x + 3; {x < 10 && y < 13}
---------------------------------------------------------------------
    {y < 5} x := y * 2; y := x + 3; {x < 10 && y < 13}

If-Then-Else Rule

选择(if-then-else)结构的程序基本语法如下。 其中B是选择判断条件，当B为真时运行S1，反之运行S2。

if B then
    S1
else
    S2

我先给出选择结构程序的基本规则If-Then-Else Rule，为了简化理解，这里我将Hoare的原规则作了不严谨的改写。 如果B为真，套用第一条规则；如果B为假，套用第二条。

{P && B} S1 {Q} 
----------------------------
{P} if B then S1 else S2 {Q}


{P && !B} S2 {Q}
----------------------------
{P} if B then S1 else S2 {Q}

我们通过一个求绝对值的例子，来理解这条规则。

if x < 0 then
    abs := -x;
else
    abs := x;

这个式子中，

  • B是x < 0，
  • S1是abs := -x;，
  • S2是abs := x;。

假如程序执行前是x等于-10，那么前置条件P就是x = -10，故x < 0为真，所以套用第一条规则我们得到：

{x = -10 && x < 0} abs := -x; {abs = 10}
------------------------------------------------------------
{x = -10} if x < 0 then abs := -x; else abs := x; {abs = 10}

While-Do Rule和Invariant

写了这么多，其实上面所有的内容都是热身运动，循环（while-do）结构的程序证明才是本文重点。

while B do
    S

到目前为止，我们讨论的所有程序都没有死循环的危险。而要证明循环结构程序的完全正确性（total correctness），我们需要证明程序的两个性质：

  • 循环可终止（termination）。
  • 循环部分正确性（partial correctness）。这个提法很费解，它实际的意思是指“如果循环最终能终止，那么这支程序会满足一定的条件”。

证明Partial Correctness

我们先讨论如何证明partial correctness， 首先需要找到一个不变条件（invariant）P，它满足如下式子（While-Do Rule）：

{P && B} S {P}
--------------------------
{P} while B do S {P && !B}

从式子里我们可以观察到，P不但在while-do整支程序执行的前后都是成立的，而且在循环内部的S的执行前后也都成立。即invairant是在整个循环执行过程中不变的性质。 另外，作为S的Precondition，B必须满足，不然循环内的代码怎么会运行呢？ 而且，作为整个循环的Postcondition，!B必须满足，不然循环怎么会结束呢？

从一个简单的例子来看，下面这个循环对1到10的整数求和。

sum := 0;
i := 1;
while i <= 10 do
     sum := sum + i;
     i := i + 1;

这里我先提前给出循环的invariant P为sum = 0 + ... + (i - 1) && i <=11。具体地说，sum满足下面

  • 当i = 1, sum = 0
  • 当i = 2, sum = 0 + 1
  • 当i = 3, sum = 0 + 1 + 2
  • 当i = 4, sum = 0 + 1 + 2 + 3
  • …

那么While-Do Rule横线上面的部分{P && B} S {P}是否成立呢？即需要证明：

{(sum = 0 + ... + (i - 1) && i <= 11) && i <= 10} sum := sum + i; i := i + 1; {sum = 0 + ... + (i - 1) && i <= 11}

我们套用Sequential Rule可以证明这个式子。

{(sum = 0 + ... + (i - 1) && i <= 11) && i <=10} sum := sum + i; {sum = 0 + ... + i && i <= 10},
{sum = 0 + ... + i && i <= 10} i := i + 1; {sum = 0 + ... + (i - 1) && i <= 11}
--------------------------------------------------------------------------------
{(sum = 0 + ... + (i - 1) && i <= 11) && i <= 10} sum := sum + i; i := i + 1; {sum = 0 + ... + (i - 1) && i <= 11}

既然我们已经证明了While-Do Rule横线以上的部分成立，那就可以得出横线以下的部分{P} while B do S {P && !B}成立。 也就是说如果循环满足P这个Precondition，循环结束后P && !B成立。那么，问题是P是否是循环的Precondition呢？ 在循环运行之前，显然我们知道sum = 0 && i = 1，根据P的定义我们得到：

sum = 0 && i = 1
=> sum = 0 + ... + (i - 1) && i <= 11

所以，循环结束时，程序将满足P && !B，即

(sum = 0 + ... + (i - 1) && i <= 11) && i > 10
=> sum = 0 + ... + (i - 1) && i = 11
=> sum = 0 + ... + 10 && i = 11
=> sum = 1 + ... + 10 && i = 11

通过推理，我们不但证明了sum最终会是1到10的和，而且知道最终i是11。

这里的讨论中，我并没有说明我们是如何得到这个invariant的式子的。比如为什么P需要有i <= 11这个条件？为什么不是i < 11？又或者sum为什么不是1 + ... + i或者1 + .. + (i + 1)，而要从0开始？

寻找invariant，需要程序员对程序逻辑的透彻理解和深入洞察力。 即使在上面这么简单的程序中，我们也可以看出找到invariant并非那么显然的过程。 在编写循环代码的过程中如果能明确地意识到invariant的存在，不只可以覆盖很多edge case，预防bug的发生，还有助于写出品味较好的代码。

证明termination

不可终止的程序，也就是俗称的死循环，比如：

while true do
    skip;

尽管停机问题是不可判定的，并不代表我们无法得知我们的循环是否会终止。 一支会终止的循环程序需要满足下面三个条件：

  1. 能找到一个特征变量n，每次循环n的值都在变小；
  2. n存在下限，即存在一个常数N使得n >= N；
  3. n的变化量不能无限趋向于0。

以上面的求和程序的例子来说，我们可以令n = - i，由于i每次循环都+ 1，所以n相应每次都- 1，故满足条件1和3。通过invariant我们知道循环始终满足i <= 11，也就是说n >= -11，故满足条件2。所以我们可以断定我们的程序是可终止的，从而证明了程序的total correctness。

通过上面的例子，我相信读者能够理解条件1存在的理由。下面两支程序说明了满足条件2的必要性：

n := -1;
while n < 0 do
    n := n - 1;

n := 1；
while n != 0 do
    n := n - 2;

尽管n满足条件1和3，但由于它不满足条件2，所以无法终止。 那么，为什么还需要满足条件3呢？ 思考下面这个程序，其中n是数学有理数。

n : = 1;
while n > 0 do
    n := n / 2;

这里的n满足条件1和2，却不满足3，故无法终止。

总结

尽管本文主要介绍了通过Hoare Logic的规则证明一些程序性质的方法，但其中关于如何推理程序正确性的思想很值得在设计以及编写程序的过程中应用。 比如动手写代码前如果能提前想好一些关键部位的Precondition/Postcondition/Invariant，编写过程往往会事半功倍； 写完代码后，再通过推理验算当初设计的这些条件是否仍然满足，便能找出一些遗漏的bug； 写完循环之后，对照termination的三个条件自查，便能找出死循环的情况。

而在面试过程中，如果平时稍有练习，几乎不会遇见思路非常困难的题目。 即使真的豪无头绪，通过和面试官沟通获得hint通常也不是减分项。 尤其就大公司的普通职位面试而言，为了公平反应面试者的基本代码能力，真正需要考察的，也不是会多么偏门的数据结构和算法，或者特殊领域的知识点。 清晰的代码思维和良好的代码习惯才是主要考核项目，毕竟大家大部分代码都在写顺序、选择和循环。 （对了，还有递归，以后有机会再写吧。）

Feedbacks are welome: @czheo