程序终止性证明的笔记

PB12011022
桑榆扬

FOPL

我的大研课题是验证一个判定C程序终止性的算法，为了准备接下来的工作，我阅读了一篇论文：Proving Program Termination。它总结了迄今为止程序终止性证明的发展情况、常用思想、重要的算法。以它为基点，可以阅读更加细节性的论文。

Introduction

程序终止性问题的定义为：在有限的时间里，判断一个程序会终止还是无限执行。它起源于希尔伯特计划：为数学提供一个严格的形式化语言。Gödel证明了该问题无解：任何相容的形式系统，只要蕴涵皮亚诺算术公理，就可以在其中构造在体系中不能被证明的真命题，因此通过推演不能得到所有真命题。另外Turing证明的停机问题和它是等价问题。

这个证明导致了相关领域研究的停滞，而实际上完全可以在有限的时间内，确定一大类程序的终止性，而对于无法判定的程序给出回答"unknown"。于是问题从回答yes/no变成了回答yes/no/unknown。

显然我们能对任何问题回答unknown，但是这显然没有什么意义。所以要尽量减少回答unknown的情况，也就是对于尽可能多的程序作出准确的判断。如今已经研发出了很多判断终止性的工具，它们只在极少的情况下回答unknown。因此已经达到了实用的级别。

许多问题可以转化为终止性判定问题。过去如果y一个科研工作者发现自己的问题和停机问题很像，就很有可能会考虑放弃当前的工作；而如今情况正好相反，他可以试图将问题转化为终止性判定问题，然后用现有的工具直接求解。

Turing在1949年的论文Checking a large routine中将终止性问题分为两类：终止论断搜索(termination argument search)和终止论断检验(termination argument checking)。

Termination argument search

将程序中的状态映射到一个良序集(well-ordered set)上。一个良序集的任意非空子集都有一个最小元素，自然数就是一个典型的良序集。如果程序在执行过程中，状态对应的元素逐渐向最小元素逼近，则无论初始值为多少，最终都会终止。

Turing曾提出一种方法：将待检测程序的每一步都映射到一个已经会确认终止的程序，从而证明它会终止。这个映射函数称为秩函数(ranking function)。迄今为止，所有的终止性证明方法实际上都使用了这种技术。真正找到这样的一个秩函数是很难的，但是一旦找到这个函数后，可以方便地判定原程序的终止性。

考虑下面一个例子，input()表示接收一个用户输入。判断它的终止性。

x := input();
y := input();
while x > 0 and y > 0 do
    if input() = 1 then
        x := x - 1;
        y := y + 1;
    else
        y := y - 1;
    fi
done

可以使用秩函数：2x+y。设当前状态为x和y，则f=2x+y，如果用户输入1，则f=2(x-1)+(y+1)=2x+y-1；如果用户输入非1，则f=2x+y-1。无论哪种情况f值都会减小。所以无论初始x和y为多少，最后2x+y都会降到0，这时x和y中至少有一个小于火等于0，从而不符合循环条件，因此程序会终止。

此外还有一种基于Ramsey's theorem的方法，可以找到多个秩函数并使用disjunctive termination arguments（下面会有例子）。这种思想也暗含在：rewriting system，logic，functional programs。
对于上述的例子，可以使用这样的终止性论断：x至少下降1并且大于0 或 y至少下降1并且大于0。
两个终止性论断通过或组合起来构成新的终止性论断。
再考虑如下的例子：

x := input();
y := input();
while x > 0 and y > 0 do
    if input() = 1 then
        x := x - 1;
        y := input();
    else
        y := y - 1;
    fi
done

直接使用第一种终止性论断不能判断它的终止性，因为这里y受input控制。而使用第二个论断就可判断其终止。

使用这种新式的终止性论断后，用户可将程序分为一些相互独立的片段，然后对每个片段构造一个秩函数，从而降低了构造秩函数的难度，但是这样做是有代价的，最终需要检验一个更困难的条件来判断终止性（接下来谈到的断言检验工具可以降低这个问题的难度）。不仅要考虑一遍循环，还要考虑每次循环时性质是否保持。

Termination argument checking

可将断言语句（如下面的assert(y>=1)）放入程序中，以检验是否满足某个条件。它能用来检测某组disjunctive termination arguments的有效性。

if y >= 1 then
    while x > 0 do
        assert (y >= 1);
        x := x - y;
    done
fi

如果一个终止性论断形式为：T1 or T2 or ... or Tn，那么如下方法可判定它的有效性：
在任何两个状态间变化时，上述T1 or T2 or ... or Tn都保持。
可以在待检测的程序中加入表示状态的变量，并且用断言语句检查前后两次迭代时是否保持性质。如果断言检验工具能证明该断言一直有效，就能确保终止性论断有效。
例如第一个例子可以使用如下的断言证明其论断的有效性：

copied := 0;
x := input();
y := input();
while x > 0 and y > 0 do
    if copied = 1 then
        assert( (oldx >= x + 1 and oldx > 0)
                or
                (oldy >= y + 1 and oldy > 0))
    elsif input() = 1 then
        copied := 1;
        oldx := x;
        oldy := y;
    fi
    if input() = 1 then
        x := x - 1;
        y := y + 1;
    else
        y := y - 1;
    fi
done

如果仅仅通过运行程序来试图判定条件是否满足，则肯定会失败，因为不可能穷尽所有的可能情况。所以断言判定工具必须能证明所有的可能情况都有效但是又不能执行所有的可能路径（因为要在有限时间内完成验证）。许多这类工具都能输出一条导致bug的路径。

Find Termination Arguments

既然能够证明终止性论断的有效性，那么如何找到终止性论断呢？

Rank function synthesis

Theorie der einfachen Ungleichungen 可以自动生成许多秩函数，我们称线性表达式构成的秩函数为简单秩函数。通过解线性约束问题可以求出它们。

Termination analysis

Variance analyses from invariance analyses 某些问题已经通过构造的方法几乎满足了disjunctive termination arguments，可用多种方法来判定它们。有时只要判断是否论断代表了一类测度。有时要猜论断然后再判定。不过这种做法会导致即使原程序不终止，判定程序也只能汇报unknown。（我看不懂这段_(:з」∠)_）

Finding arguments by refinement

Termination proofs for systems code 通过找反例，可以修正它们得到秩函数。

Further Directions

Dynamically Allocated Heap

考虑如下例子，判断它是否终止：

c = head;
while (c != NULL) {
    if (c -> next != NULL && c -> next -> data == 5) {
        t = c -> next;
        c -> next = c -> next -> next;
        free(t);
    }
    c = c -> next;
}

这个问题的难点在于程序种没有显式的数字变量，从而不能直接映射到自然数集上。常见的解决方法是使用形状分析工具（自动发现数据结构的形状），创建针对数据结构大小的辅助变量，从而构建秩函数。然而该方法能否实施取决于形状分析工具的正确性和效率。

Binary executables

迄今为止我们都在讨论源代码层次的终止性，但是实际上源代码还要通过编译器转化为二进制文件才能执行。所以可能需要讨论后者的终止性，可以先证明源文件的终止性，然后找到源文件到二进制文件到映射关系，从而证明后者的终止性。

Non-linear systems

如今的终止性证明工具基本上都无视了非线性的计算。比如之前我们看到的都是一些对变量的加减这些线性的运算，但是如x:=y*z都比较难处理，所以这些证明工具都将非线性运算转化为类似x:=input()的指令。如果转化后能证明终止，则显然转换前也终止；但是可能原文件是终止，但是转化后就只能判断为unkown。该方向已有了一些初步的研究，但是仍有很多工作要做。

Concurrency

分析并发程序时，还有考虑多线程的各种交织情况。现在的常见方法是使用rely-guarantee或assume-guarantee，在限制了环境的情况下单独考虑每个线程，从而避免了考虑所有线程交织的情况。

Advanced programming features

如今业界的程序中都还有一些高级的特性：虚函数、继承、高阶函数、闭包等。它们会增加终止性证明的难度，而且该领域尚待发掘。
无类型和动态类型程序也会增加证明的难度，因为如今的研究都基于静态的分析。此外，现在急需对于JavaScript的终止性证明。

Finding preconditions that guarantee termination

如果一个程序不保证不终止，但是添加了某些条件后就终止了，则最好能自动地找到这些前条件。然而即使是简单程序的最弱的前条件，也只能用非常复杂的方式表达，而当前的证明工具都不支持这种表达。另外提升找到前条件的速度也是一个挑战。该领域已有了一些初步地进展。

Dynamic analysis and crash dumps for liveness bugs

本文仅讨论了静态的、编译时的证明技术，运行时的证明技术尚有待发掘。已有人研究了在运行阶段自动检测死锁的方法。临时改变调度策略等技术，即使不一定能保证终止，但是可以保证不出现死锁。该方法尚待发掘。

Scalability, performance, and precision

如今最好等证明工具最多只能处理30000行的代码，另外也不能保证精度。尽管终止性是不可判定的，但是这并不阻止我们增加某类问题的判定精度，如Collatz problem，也就是著名的3n+1问题，该问题的终止性不可判定。我认为可以尽管某些问题就是不可判定，但是可以检测出它属于哪类不可判定问题。