
318
|
第 9 章
我們從型別系統獲得的任何資訊都不能盡信,而且在決定要相信多少的時候,也必須注
意它的極限。成功執行程式的靜態語意並不代表『這個程式一定能運作』,只是『這個
程式的確不會以特定的方式失敗』。能有這樣的自動化系統的確很棒,因為它可以告訴
我們程式沒有任何可能的臭蟲或錯誤,但正如我們在第 8 章所看到的,事情偏偏就是那
麼不巧。
應用
本章描繪了抽象解譯的基本概念(使用低廉的近似來學習昂貴運算的行為),並示範了
簡單的型別系統,作為近似對分析程式是如何有用的範例。
我們對抽象解譯的討論相當非正式。嚴格來說,抽象解譯是一種正式且正規的數學技
術,在這種技術裡將相同語言的不同語意,透過將一組具體的值轉換成抽象的值(反之
亦然)的函數相互連接,進而能以具體的值來瞭解抽象程式的結果和特性。
這種技術最知名的業界應用是 Astrée 靜態分析儀(
http://www.astree.ens.fr/
),它使用抽
象解譯來自動查驗 C 程式沒有諸如除以零、陣列索引超越邊界、整數溢位等執行階段
錯誤。Astrée 已經用在驗證空中巴士 A340 和 A380 飛機的飛行控制軟體,以及運補到
國際太空站的
Jules Verne
ATV-001 飛行任務的自動對接軟體。抽象解譯顧及萊斯定理
的方式,就是提供安全的近似,而非肯定的答案,所以 Astrée 回報的執行階段錯誤,
實際上可能不存在(誤警 [
false alarm
]);實際上,它的抽象體精確度在驗證 A340 軟體
時,已足以避免任何誤警。
以 SIMPLE ...