safety-critical

静态分析无法证明你的飞机不会坠毁。但它能证明一些更有用的东西。

抽象解释会对每一种可能的程序状态进行过度近似。如果除零错误在抽象中不可达，那它在真实代码中就不可达。以下是它的工作原理以及它的局限性。

静态分析无法证明飞机不会坠毁。但它可以证明你的高度计控制回路永远不会出现除零运算、永远不会越界索引、永远不会使定点累加器溢出。这种区别很重要，因为前者是对物理、空气动力学和铝材在应力下的断言，而后者是对代码的断言——你可以在飞机离地之前就验证它。…