C专家编程 第10章 再论指针 10.8 轻松一下---程序检验的限制

工程师所存在的问题是他们采取欺骗手段以获取结果
数学家所存在的问题是他们研究一些玩具性的问题以获得结果
程序检验员所存在的问题是他们在玩具性的问题上采取欺骗手段以获得结果。---匿名人士

不使用临时变量交换两个值
有人问我下面的程序段（用于交换两个值）能否达到目的：
*a ^= *b; /*执行3个连续的异或操作*/
*b ^= *a;
*a ^= ^b; 

在满足下面两种标准的前提下执行下面这个序列：这几个操作都是原子操作；它在执行时不会发生硬件失败、内存空间不够或数学运算失败等问题。
*a ^= *b; *b ^= *a; *a ^= ^b;
之后，*a和*b的值将是f3(a)和f3(b)。其中，
f3 = lambda x.(x == a ? f2(a) ^ f2(b) : f2(x));
f2 = lambda x.(x == b ? f1(b) ^ f1(a) : f1(x));
f1 = lambda x.(x == a ? *a ^ *b : *x);
这样一来，这段代码只会产生两种结果（源于beta reduction），即
如果a和b相同：f3(a) = f3(b) = 0
如果a和b不相同：f3(a) = b, f3(b) = a;
数学检验和验证是唯一可靠的技巧。否则的话，程序就是工程黑客的作品罢了。与人们想象的相反，所有的C程序都容易根据这种方法通过数学分析来进行驾驭。
也就是： 
如果a和b相同：f3(a) = f3(b) = 0
如果a和b不相同：f3(a) = b, f3(b) = a;
实际上应该是：
f3(a) = *b，且f3(b) = *a... 

不仅这个检验存在两个错误，而且它所“检验”的C程序事实上也不正确！大家都知道在C语言中不可能不使用临时变量来交换两个值（在一般情况下）。在此例中，如果a和b指向重叠的对象，这个算法就会失败。另外，如果其中一个变量存储于寄存器中或者是一个位段，这个算法也不可行，因为无法取得寄存器地址或者位段的地址。如果*a和*b是长度不同的类型，或者它们其中之一指向一个数组，该算法同样不行。

程序检验的问题，可以阅读一篇文章Social Precessed and Proofs of Theorems and Programs，刊登于Communications of the ACM。