软件故障率与半形式化设计验证
软件故障的本质与可预测性
在软件领域，我们常常遇到一些看似随机的故障。例如，有一个程序运行100万次后，变量x的值始终如预期般处于100到200之间，但实际上该程序可能存在故障。从某种角度看，图5.4中的程序包含一个漏洞，程序员本应该用互斥锁来保护全局变量x。然而，每个发布的程序都可能存在漏洞，我们应该面对现实，而不是幻想一个没有难以捉摸的“海森堡漏洞”（Heisenbugs）的完美世界。
对于软件的统计性故障，我们可以进行类似的思考。就像我们无法预测一个机械弹簧下一次使用时是否会失效，并非因为它本质上不可预测，而是因为我们掌握的信息不足。如果我们知道弹簧中每个分子的位置和速度，对其环境（如温度等）有全面的了解，并且有足够强大的计算机进行计算，原则上（在量子效应范围内）我们可以预测它下一次使用时是否会失效。软件故障也是如此，如果我们知道程序环境中每个线程的状态，并且拥有足够的计算能力，就可以精确确定程序在特定执行过程中是否会失败。但遗憾的是，当程序与库和操作系统结合时，图5.4中程序可能处于的状态数量超过了10的100次方，远远多于宇宙中的核子数量。这表明软件和硬件故障要么是真正随机的，要么是可预测的，但由于我们的无知而看起来是随机的。这种观点将当今的多线程软件与机械硬件归为同一类别，使得硬件故障分析中使用的技术也可应用于软件。
编译器和硬件对软件的影响
编译器和硬件对软件的执行也有着显著的影响。如果全局变量x的声明中没有使用volatile关键字，编译器可能会完全移除循环，并“悄悄”地将其替换为类似x = x + 100;的代码。例如，当一个没有volatile关键字的程序使用 -Os 命令行为ARM处理器编译时，生成的汇编
