safety-critical

靜態分析無法證明你的飛機不會墜毀，但它能證明更有價值的事

抽象解釋會對每一個可能的程式狀態進行過度近似。如果除零錯誤在抽象層中無法觸及，那麼在真實程式碼中也同樣無法觸及。以下是它的運作原理與局限性。

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