Proj THUDBFuzz Paper Reading: 北京大学软件分析课程2019，熊英飞, 01 intro

能否彻底避免软件中出现缺陷？

Testing shows the presence, not the absence of bugs -- Dijkstra
首先从整个图灵机的所有潜在程序来说，bug是不可能完全被找到的，
首先引入Hilberts Program，那么Hilber's Program是什么呢？
它是由德国数学家大卫希尔伯特在20世纪20年代提出，
目标是提出一个形式系统，能够覆盖现在所有的数学定理，并且满足如下条件：

1. 完备性：所有真命题都可以被证明
2. 一致性：一个命题要么是真，要么是假
3. 可判断性：存在算法来确定任意命题的真假

而哥德尔则证明了哥德尔不完备定理，主要内容是蕴含皮亚诺算数公理的一致系统必然是不完备的，可以理解为证明对任意表示自然数的系统，一定有定理不能被证明。
这与软件缺陷有什么关系呢？首先主流程序语言的语法使得程序语言能够表示任意自然数（我们考虑bigInteger类和一个近乎无限的内存），那么，假设有表达式T不能被证明是永远为true或者永远为false，对于如下的代码，就可能造成内存泄漏。

a=malloc()
if (T) free(a);
return;

一般程序员或者静态分析工具是明确在合法输入的情况下T都会为true才会写出这种代码的。
可是在什么情况下连程序员或者静态分析工具被证明绝不可能确定T到底是否为true呢？
引入停机问题，即判断是否存在算法H(P, I)可以判断对于程序P在输入I的情况下是否可停机。显然，程序本身也是一种数据，因此它可以作为输入。

void func(Program p) {
      if (H(p, p)=="halt") loop{};
      else return;//halt
}

显然func(p)的停机状态是H(p, p)简单取反，那么此时如果我们调用H(func, func)，其结果就应该是H(func,func)的取反，产生矛盾。
因此，调用自身的取反就是一个简单的不可判定问题，它证明了我们如果考虑全部潜在的程序，连判断小小的内存泄漏都难以做到，只能给出警告，不能证明这就是bug。

标签：01,取反,证明,熊英飞,THUDBFuzz,Program,内存,func,true
来源： https://www.cnblogs.com/xuesu/p/14220320.html