这么哲学的问题，不知道该从哪里扯起啊。
图灵停机
假设我是一个”内裤收集狂魔“，咳...不是，是”程序收集狂魔“，喜欢收集各式各样的程序，于是，每天世界各地的程序员都给我发来他们写的各种奇葩程序。我作为一个收藏家，起码要判断一下他们发来的程序是否可以在特定的输入下正常结束退出，要知道，有很多学渣写的程序会不明不白地陷入死循环，无响应之类的，这种程序我就没必要收藏了。
但是，每天收到的程序太多了，根本不可能一个一个手工去试它们能不能正常结束。我作为学神，当然希望写一个判断程序，来帮助我去自动测试这些程序，把不能正常结束的程序都挑出来。那么问题来了，我能不能写出这样的程序呢？
图灵告诉我说，不能。图灵停机问题描述的是：是否存在一个程序，它能够计算任何程序在给定输入下是否会运行结束。
假设我文曲星附身，灵光大闪，真的写出这样一个程序，那么就先假设有这样一个函数，名字是 CheckHalt(program, input)，那么程序写出来大致就是这样。
bool CheckHalt(program, input)
{
if(program halts on input)
return true;
else
return false;
}
逻辑一目了然，就是如果被检测的程序在给定的输入下停机了，就返回真，表明可以停机，否则，就返回假，表明不能停机。此时，再构造一个自己给自己找病的函数 Check，参数是一个程序：
void Check(program)
{
if(CheckHalt(program, program))
while(1);
else
return;
}
这个时候，来考虑一下Check(Check) 是否会停机（就是正常退出），就是说自己调用自己的情况。
- 如果
Check(Check)可以停机，那么一定走的是else分支，那么if(CheckHalt(program, program))应该判断为假。也就是说，CheckHalt(program, program)返回的是 false，即程序不可以停机，与假设能停机是矛盾的。 - 如果
Check(Check)不可以停机，也就是说，它陷入了while(1);的死循环，则if(CheckHalt(program, program))返回的是 true，即程序可以停机，与假设又是矛盾的。
所以，灵光大闪是瞎闪，文曲星也没附身，这样的程序根本不存在。
像给你一个输入 x，你写个函数，给我计算以 x 为半径的圆的面积，这种能用编程语言写出来并且运行的，都是可计算函数。考虑的更一般化一些，函数就像个黑盒一样，你给它喂一个输入，它就会吐一个输出。那么在 Windows 系统上运行的可执行程序，某种角度看也是函数，你运行任何程序，都是你给它一个指令（输入），它做出预设好的反应（输出），比如你点右上角的红叉，那窗口会关闭。处理同一类问题有相同的算法，这样的函数是可计算函数。
另外就是，如果一个程序 P 的效果和一个函数关系 f 的效果一样，那么就说 P 可以计算 f，f 是确定的，然而 P 却可以有 N 多个。比如给出半径求圆面积，这个计算公式，也就是函数关系 f(x) = Pi * r * r 是死的，是确定的。但是全班每个人写出的程序可能都不一样，有的人会多用几个中间变量，有的人会多输出几个字使程序更加友好等等。
以上是可计算函数，而像图灵停机问题这种，就是不可计算函数，或者说是不可判定的。不可计算函数也有很多，比如，不存在一个程序，它能够判断任意两个程序是否能计算同样的 f。
Rice 定理
世界上函数这么多，怎么才能判断某个函数是不是可计算呢。Rice 定理可以帮到我们。Rice 定理说的是：有一个函数集合 S （就是说 S 是函数关系 f 的集合），并且 S 不是空集，也不是全部函数 f，那么程序 P 是否属于 S 是不可计算的。
这到底啥意思？
比如计算圆面积的公式是一个函数，那么假定集合 S 就包含这一个元素，显然 S 不是空集也不是全部函数，那么如果我想写一个自动判作业程序，自动判断学生交上来的作业程序 P 是否正确计算了这个圆面积，这样的判作业程序是不存在的。
这可能和现实的感觉不一样，你会感觉好像有这样的程序，其实不是，现实中的确可以写出来，但写出来的程序会有误判，因为这是一个不可计算问题，现实的解决方案只能做到近似。现实生活中有非常多的具有判别功能的程序，存在着误报和漏报，因为它们解决的都是不可计算问题，这些程序做的，只是权衡误报率和漏报率，根据需要给出一个较优解。
回到静态分析
静态分析的文章，引用 Rice 定理，无非是想说明，完全准确的静态分析程序是不存在的，或者说普适的静态分析算法，静态分析工具是不存在的。
- 世界上不存在一个程序，可以检测任何程序 P 是否具有某个安全漏洞。
- 世界上不存在一个程序，可以检测任何程序 P 是否进入了某个 if 分支。
- 世界上不存在一个程序，可以检测任何程序 P 是否...
所以文章中 (《基于静态分析的安全漏洞检测技术研究》) 会说：由于程序的任何非平凡性质都是不可判定的，所以静态分析算法只能给出源程序某些性质的不完全或不精确的解。
上一篇文章， Splint 给出分析结果时用的动词都是 may （去看看图片，是不是 may），最后它分析的对不对，还是需要人来判断的。
