答案是「不行」。真正的問題是：它能證明什麼？

靜態分析無法證明飛機不會墜毀。但它可以證明你的高度計控制迴路絕不會發生除零、絕不會陣列索引越界，也絕不會讓定點累加器溢位。這兩者之間的區別至關重要：前者是關於物理、空氣動力學，以及鋁合金在壓力下的主張；後者則是關於你可以在飛機離地前就驗證完的程式碼。

這就是抽象解釋的承諾。不是全知全能，而是嚴謹的證明——證明某些特定類別的災難性軟體故障，在任何可能的執行路徑中都不會發生。

為什麼測試了百萬種情境，你仍然只是在猜

一套典型的飛行控制系統包含數十萬行 C 語言程式碼。輸入空間是感測器讀數、駕駛指令、環境條件與內部狀態變數的笛卡兒積。你可以讓系統在模擬器中執行到宇宙熱寂，仍然無法覆蓋所有路徑。

測試能找到 bug，但無法證明 bug 不存在。每一個通過的測試都只是數據點，不是保證。

抽象解釋顛覆了這個做法。它不是用特定輸入來執行程式，而是在「抽象領域」（abstract domains）上執行程式，這些抽象領域代表了所有可能的數值集合。如果抽象分析指出某個錯誤狀態無法觸及，那麼對於每一個具體輸入來說，該錯誤都同樣無法觸及。這個證明是窮盡的，因為它只需一次遍歷就能涵蓋整個輸入空間。

具體數值太昂貴了。改用形狀來表示。

考慮一個簡單的變數 x。在具體執行中，x 可能是 42；在抽象解釋中，x 可能是「0 到 255 之間的任意整數」。這稱為區間抽象（interval abstraction）。

分析器會追蹤這些區間在每一個運算中的變化。如果 x 是 [0, 100] 而 y 是 [1, 10]，那麼 x / y 就是 [0, 100]。分析器知道除法是安全的，因為除數的區間不包含零。

但如果 y 是 [-5, 5]，分析器就會標記出潛在的除零風險。它不知道具體執行是否真的會碰到零，但它知道零落在可能的範圍內。這就足夠觸發警報了。

這個核心洞見來自 Patrick 與 Radhia Cousot 在 1976 年的研究：抽象領域必須是具體語義的可靠過度近似（sound over-approximation）。每一個具體行為都必須能在抽象層中被表達。如果抽象層是安全的，具體程式就是安全的；如果抽象層發出警告，具體程式也許沒問題——但也許有。

用 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 是有上限的。分析器在合併點（merge points）會失去精確度——也就是兩條控制流路徑交匯、它們的抽象狀態必須被合併的地方。

真正的工具會使用更複雜的領域。多面體（polyhedra）、八邊形（octagons）與謂詞抽象（predicate abstractions）會追蹤變數之間的關係。區間看不到 x < y，但多面體領域會記住它。這些領域更精確，但也更昂貴。多面體領域在最壞情況下具有指數級複雜度。對於一套三十萬行 C 語言的飛行控制系統來說，一個簡陋的實作可能在這架飛機退役之前都還算不完。

Astrée 在 A380 上實際證明了什麼

Astrée 是讓抽象解釋在航空界聲名大噪的靜態分析器。2003 年，Astrée 被用於分析空中巴士 A380 的主飛行控制軟體。它證明了該軟體不存在任何執行期錯誤：沒有除零、沒有陣列越界存取、沒有算術溢位、關鍵路徑中也沒有無法觸及的程式碼。

它並沒有證明飛機不會墜毀。它沒有證明控制律是正確的。它也沒有證明攻角計算符合該飛機的物理特性。這些是不同的問題，需要用不同的工具來解決。

Astrée 證明的是軟體不會自我崩潰。這個主張聽起來很狹隘，但比大多數人想像的更有價值。軟體自我毀滅是航空事故的常見原因。能證明它不會發生，這份努力是值得的。

這套工具透過結合多種領域專屬的技巧達成了這個成果。它使用非關聯式領域來換取速度，並使用關聯式領域來確保精確度。它用一個納入捨入誤差的模型來處理浮點運算。它理解航電中使用的特定 C 語言子集，並將未定義行為視為錯誤。工程師花了數年時間調校，才將誤報率降到足夠低，讓工程師願意信任它的輸出。

可靠性是一種選擇，不是預設值

並非所有靜態分析器都追求可靠性。像 Coverity、CodeQL 和 Infer 這類工具，優先考慮找到真正的 bug，而非證明 bug 不存在。它們對狀態空間進行低度近似（under-approximate）。它們可能會漏掉某個除零錯誤，但它們找到的通常是真的。

這是合理的工程選擇。對於網頁應用程式來說，一個能在幾分鐘內執行完畢、準確率 90% 的 bug 查找工具，勝過一個讓你淹沒在誤報中的可靠分析器。但對於飛行控制系統來說，情況正好相反。你想要的是證明，即使你必須過濾雜訊。

抽象解釋是讓這種證明成為可能的技術。但它不是唯一的正規方法。像 SPIN 和 TLA+ 這樣的模型檢查器（model checkers）用來驗證狀態機。像 Coq 和 Isabelle 這樣的定理證明器（theorem provers）用來驗證功能正確性。抽象解釋佔據了一個甜蜜點：它完全自動化、能擴展到大型 codebases，並且能對執行期行為給出數學上的保證。

抽象解釋的極限在哪裡

這個方法有著嚴格的極限。它無法對透過複雜指標運算所配置的記憶體進行推理。它無法驗證你的演算法是否計算出正確的數值，只能驗證它在計算過程中不會崩潰。它在面對並行處理、動態分派，以及刻意依賴未定義行為的程式碼時也會力不從心。

它還要求程式碼必須以可驗證的風格來撰寫。A380 的飛行軟體避免遞迴、限制動態記憶體配置，並保持控制流簡單。這些限制不是分析器的缺陷，而是證明的前置條件。你無法為太過混亂而無法建模的程式碼證明任何性質。

從真實函式的區間分析開始

你不需要 Astrée 就能應用這些想法。從你的 codebase 中挑選一個單純的函式（pure function）。找出一個必須保持在範圍內的變數。寫一個簡單的區間傳播腳本，追蹤這個變數在每一個分支與運算中的變化。

如果在使用點的區間落在安全範圍內，你就擁有了一個針對該變數的手動安全性證明。如果不是，你就發現了一個 bug，或是發現自己的推理有所遺漏。無論是哪一種，你都學到了單元測試可能無法發現的東西。

抽象解釋無法證明你的飛機不會墜毀。沒有任何東西做得到。但它可以證明，你的軟體不會是導致墜機的原因。

常見問題

什麼是抽象解釋？

抽象解釋是一種靜態程式分析的正規方法，它用具象徵性的抽象表示（例如區間或形狀）來取代具體的程式數值。分析器在這些抽象數值上模擬程式執行。如果某個錯誤在抽象領域中無法觸及，那麼在具體程式中，對於所有可能的輸入，該錯誤也同樣無法觸及。

抽象解釋能找到所有 bug 嗎？

不能。抽象解釋證明的是特定執行期錯誤不存在，例如除零、緩衝區溢位與算術溢位。它無法驗證演算法是否產生正確結果，只能驗證它不會崩潰。它也無法對程式碼以外的性質進行推理，例如硬體故障或物理系統的行為。

可靠（sound）與不可靠（unsound）的靜態分析有何不同？

可靠的分析器會對所有可能的程式行為進行過度近似（over-approximate）。它絕不會漏掉它設計要偵測的類型的 bug，但可能會回報誤報。不可靠的分析器則進行低度近似（under-approximate）。它可能會漏掉 bug，但它回報的 bug 更有可能是真的。可靠性對安全關鍵系統至關重要；而一般軟體開發中，為了更快得到回饋，通常偏好使用不可靠的分析。

抽象解釋只適用於安全關鍵軟體嗎？

不是，雖然那是它最常被使用的地方。抽象解釋背後的想法也出現在許多編譯器與最佳化器中。例如，LLVM 的範圍分析（range analysis）就使用區間抽象來消除多餘的邊界檢查。你可以將同樣的區間推理應用在任何需要證明邊界的程式碼上，從嵌入式韌體到高效能數值核心都不例外。