算法算法分析

霍尔三元组、循环不变式与程序正确性

字数统计: 1.2k字   |   阅读时长: 4分
,

摘要: 循环不变式

【对数据分析、人工智能、金融科技、风控服务感兴趣的同学，欢迎关注我哈，阅读更多原创文章】
我的网站：潮汐朝夕的生活实验室
我的公众号：潮汐朝夕
我的知乎：潮汐朝夕
我的github：FennelDumplings
我的leetcode：FennelDumplings

托尼·霍尔(1934-)

托尼·霍尔 (Hoare) 是 20 世纪非常有影响力的一位计算机科学家，1980 年图灵奖。我们熟知的快速排序算法正是霍尔在 1960 年发表的。1972 年他与 O.J. Dahl 和 E. W. Dijkstra 三位图灵奖得主合著的《Structured Programming》一书，也很有名。

1969 年 10 月，霍尔发表了有里程碑意义的论文“计算机程序设计的公理基础”。在这篇论文中，霍尔提出了公理语义学，放弃了流程图并开发了一个逻辑系统来推理程序，这个逻辑系统称为霍尔逻辑。这是继 1963 年用递归函数定义程序，以及在 1967 年基于程序流程图的归纳断言法(Floyd)之后，程序逻辑研究中所取得的又一个重大技术进展。

霍尔逻辑系统为使用严格的数理逻辑推理计算机程序的正确性提供一组逻辑规则。本文我们简要了解一下霍尔逻辑，以及如何用循环不变式验证程序的正确性。

霍尔三元组

霍尔三元组描述一段代码的执行如何改变计算的状态，形式如下:

其中 P 和 Q 是断言，C 是命令，P 称为前条件，Q 称为后条件。其含义是“只要 P 在 C 执行前的状态下成立，则执行之后 Q 也成立”。

如果 $C$ 是一个循环，循环有一个退出条件，以 while 循环为例，如果当 $B$ 成立时，执行 $S$，当 $B$ 不成立时，退出循环，那么循环不变式对应的霍尔三元组可以写为：

也就是“$P$ 在循环 while B do S done 之前的状态下成立，则执行之后，$\urcorner B \land P$” 也成立。

命令中的循环条件可以放到前条件中，例如下面这个霍尔三元组与前面的是等价的：

也就是“$P \land B$”在$S$执行前的状态下成立，则执行之后 $P$ 成立。

下面看一个具体的例子：

则下面两个霍尔三元组等价：

循环不变式

循环不变式是在循环体的每次执行前后均为真的谓词，循环不变式体现了循环程序中循环变量的变化规律。

比如对于插入排序，循环的过程中，“A[0..j-1] 始终是有序的”是一个循环不变式。

对于循环不变式 $P$，我们需要证明三件事：

  • 初始：循环的第一次迭代，$P$ 为真
  • 保持：如果循环的某次迭代之前 $P$ 为真，则下次迭代之前 $P$ 也为真
  • 终止：在循环终止时，不变式提供一个有用的性质，有助于证明算法的正确性

循环不变式可以用于分析程序正确性。下面以插入排序为例，来看一下具体怎么用。

程序正确性（例子：插入排序）

伪代码：首先给出插入排序的伪代码。

1
2
3
4
5
6
7
8
for j = 2 to A.length:
    key = A[j]
    // insert A[j] into the sorted sequence A[1..j-1]
    i = j - 1
    while i > 0 and A[i] > key
        A[i + 1] = A[i]
        i = i - 1
    A[i + 1] = key

循环不变式：在 for 循环的每次迭代开始时，子数组 A[1..j-1] 由原来在 A[1..j-1] 的元素组成，但已排好序。

初始：第一次循环迭代之前 A[1..j-1] 仅由单个元素 A[1] 组成，它是原数组 A[1] 的元素，且已排序好的。循环不变式成立。

保持：伪代码中第 4 ~ 7 行将 A[j - 1], A[j - 2], A[j - 3] 向右移动一个位置，直至找到 A[j] 的适当位置，第 8 行将 A[j] 插入该位置。此时 A[1..j] 由原数组 A[1..j] 的元素组成，且已排好序，于是 for 循环的下一次迭代增加 j 将保持循环不变式。

终止：导致 for 循环终止的条件是 j > A.length，因为每次迭代 j 增加 1，因此 j = n + 1。在循环不变式的表述中将 j 用 n + 1 代替，有：子数组 A[1..n] 中的元素组成，但已排好序。而 A[1..n] 就是整个数组，因此整个数组已经排好序。因此算法正确。

Share