答案是“不能”。真正的问题是，它能证明什么。

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

这就是抽象解释的承诺。不是全知全能，而是严格证明：在每一种可能的执行中，特定类别的灾难性软件故障都不可能发生。

为什么测试一百万个场景仍然让你心里没底

一个典型的飞控系统包含数十万行 C 代码。输入空间是传感器读数、飞行员指令、环境条件和内部状态变量的笛卡尔积。你可以在模拟器里运行这个系统直到宇宙热寂，仍然无法覆盖所有路径。

测试能发现 bug。但它不能证明 bug 不存在。每一次通过的测试都是一个数据点，而不是保证。

抽象解释扭转了这种思路。它不是用具体输入来执行程序，而是在表示可能值集合的抽象域上执行程序。如果抽象分析表明某个错误状态不可达，那么对于每一个具体输入，该错误都不可达。这个证明是穷尽的，因为它在一次分析中就覆盖了整个输入空间。

具体值太贵了。用“形状”来代替。

考虑一个简单的变量 x。在具体执行中，x 可能是 42。在抽象解释中，x 可能是“0 到 255 之间的任意整数”。这被称为区间抽象。

分析器会追踪这些区间在每一次操作中的变化。如果 x 是 [0, 100]，y 是 [1, 10]，那么 x / y 就是 [0, 100]。分析器知道除法是安全的，因为除数的区间不包含零。

但如果 y 是 [-5, 5]，分析器就会标记出潜在的除零风险。它并不知道具体执行是否真的会碰到零。它只知道零落在可能的范围内。这就足以触发警报。

关键洞察来自 Patrick 和 Radhia Cousot 于 1976 年的工作：抽象域必须是对具体语义的可靠过度近似。每一种具体行为都必须能在抽象中表示。如果抽象是安全的，具体程序就是安全的。如果抽象发出警告，具体程序可能没问题——但也可能有问题。

用 Python 实现一个玩具级区间分析器

下面是一个可用的区间抽象域实现。它很朴素，但能展示基本原理。

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class Interval:
    lo: int
    hi: int

    def __post_init__(self):
        if self.lo > self.hi:
            raise ValueError("Empty interval")

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lo + other.lo, self.hi + other.hi)

    def div(self, other: "Interval") -> Optional["Interval"]:
        if other.lo <= 0 <= other.hi:
            return None  # Potential division by zero
        # Simplified: assumes positive divisor for demo
        return Interval(self.lo // other.hi, self.hi // other.lo)

    def intersect(self, other: "Interval") -> Optional["Interval"]:
        lo = max(self.lo, other.lo)
        hi = min(self.hi, other.hi)
        if lo > hi:
            return None
        return Interval(lo, hi)

    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"


def analyze_division(a: Interval, b: Interval) -> None:
    result = a.div(b)
    if result is None:
        print(f"ALERT: {a} / {b} may divide by zero")
    else:
        print(f"SAFE: {a} / {b} = {result}")

运行几个例子：

analyze_division(Interval(10, 20), Interval(2, 5))   # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1))  # ALERT
analyze_division(Interval(10, 20), Interval(0, 5))   # ALERT

第一个例子是安全的，因为所有除数都是正数。第二个被标记，因为零在 [-1, 1] 内部。第三个被标记，因为零在 [0, 5] 内部。

注意第三个例子中发生了什么。具体程序可能永远不会真正以 b = 0 执行。分析器并不知道这一点。它是保守设计的。这是根本性的权衡。

误报的代价

一个可靠的静态分析器永远不会漏掉 bug。如果崩溃是可能的，它就会报告。但它也会报告实际上不可能的崩溃。这些误报就是可靠性的代价。

在实践中，这个代价很高。对于一个像 for (i = 0; i < n; i++) 这样的循环，朴素的区间分析经常会得出 i 是 [0, +∞] 的结论，即使 n 是有界的。分析器在合并点会丢失精度——两条控制流路径汇合时，它们的抽象状态必须被合并。

真正的工具使用更复杂的域。多面体、八角形和谓词抽象可以追踪变量之间的关系。x < y 对区间来说是不可见的，但多面体域能记住它。这些域更精确，但也更昂贵。多面体域的最坏情况复杂度是指数级的。对于一个有 30 万行 C 代码的飞控系统，朴素的实现可能在飞机退役之前都算不完。

Astrée 在 A380 上实际证明了什么

Astrée 是让抽象解释在航空领域声名鹊起的静态分析器。2003 年，Astrée 被用于分析空客 A380 的主飞控软件。它证明了不存在任何运行时错误：没有除零、没有数组越界、没有算术溢出、关键路径上没有不可达代码。

它没有证明飞机不会坠毁。它没有证明控制律是正确的。它没有证明攻角计算与飞机的物理特性相符。那些是不同的问题，需要用不同的工具来解决。

Astrée 证明了软件自身不会崩溃。这个说法听起来范围很窄，但比大多数人意识到的更有价值。软件自毁是航空事故的常见原因。证明它不可能发生，值得付出这样的努力。

该工具通过结合几种领域特定的技巧实现了这一目标。它使用非关系域来保证速度，使用关系域来保证精度。它用一个考虑了舍入误差的模型来处理浮点运算。它理解航空电子中使用的特定 C 语言子集，并将未定义行为视为错误。经过多年的调优，误报率才降到足够低，让工程师愿意信任它的输出。

可靠性是一种选择，而不是默认设置

并非所有静态分析器都追求可靠性。Coverity、CodeQL 和 Infer 等工具优先发现真正的 bug，而非证明其不存在。它们对状态空间进行欠近似。它们可能会漏掉除零错误，但它们找到的通常是真的。

这是一个合理的工程选择。对于一个 Web 应用来说，一个 90% 准确、几分钟就能跑完的 bug 查找工具，胜过把你淹没在误报里的可靠分析器。但对于飞控系统来说，恰恰相反。你需要证明，即使你得过滤掉噪声。

抽象解释是使这种证明成为可能的技术。它不是唯一的形式化方法。SPIN 和 TLA+ 等模型检验器验证状态机。Coq 和 Isabelle 等定理证明器验证功能正确性。抽象解释占据了一个甜蜜点：它是全自动的，能扩展到大型 codebases，并且能对运行时行为给出数学上的保证。

抽象解释的硬边界

这种方法有严格的限制。它无法对通过复杂指针运算分配的内存进行推理。它无法验证你的算法是否计算出正确的值，只能验证它在计算过程中不会崩溃。它在并发、动态分派以及有意依赖未定义行为的代码面前表现挣扎。

它还要求代码以可验证的风格编写。A380 飞控软件避免使用递归，限制动态内存分配，并保持控制流简单。这些限制不是分析器的局限，而是证明的前提条件。你无法为过于混乱而难以建模的代码证明任何性质。

从一个真实函数开始，用区间分析试试

你不需要 Astrée 也能应用这些思想。在你的 codebase 中挑一个纯函数。找出一个必须保持在边界内的变量。写一个简单区间传播脚本。追踪这个变量在每一条分支和每一次操作中的变化。

如果该变量在使用点的区间位于安全范围内，你就对这个变量有了手动的安全性证明。如果不是，你就发现了一个 bug，或者发现了一个你推理不完整的地方。无论哪种情况，你都学到了一些单元测试可能遗漏的东西。

抽象解释无法证明你的飞机不会坠毁。没有什么能证明这一点。但它可以证明，你的软件不会是坠毁的原因。

常见问题

什么是抽象解释？

抽象解释是一种静态程序分析的形式化方法，其中具体的程序值被抽象表示（如区间或形状）所替代。分析器在这些抽象值上模拟程序执行。如果某个错误在抽象域中不可达，那么对于所有可能的输入，它在具体程序中也不可达。

抽象解释能找出所有 bug 吗？

不能。抽象解释只能证明特定运行时错误的不存在，例如除零、缓冲区溢出和算术溢出。它无法验证算法是否产生了正确的结果，只能验证它不会崩溃。它也无法对代码之外的性质进行推理，例如硬件故障或物理系统行为。

可靠与不可靠的静态分析有什么区别？

可靠的分析器对可能的程序行为集合进行过度近似。它永远不会漏掉它设计要检测的类型的 bug，但可能会报告误报。不可靠的分析器进行欠近似。它可能会漏掉 bug，但它报告的更可能是真的。可靠性对安全关键系统至关重要。不可靠的分析通常在一般软件开发中更受青睐，因为反馈更快。

抽象解释只适用于安全关键软件吗？

不是，虽然那是它最广泛应用的领域。抽象解释背后的思想出现在许多编译器和优化器中。例如，LLVM 的区间分析使用区间抽象来消除冗余的边界检查。你可以将同样的区间推理应用于任何需要证明边界的代码，从嵌入式固件到高性能数值内核。