runtime-errors

如何證明你的程式沒有執行時錯誤（以及為什麼你很可能會放棄嘗試）

抽象解釋讓你在執行前就能證明執行時錯誤不可能發生。以下說明它實際上如何運作、為什麼很困難，以及它在你的工具鏈中扮演什麼角色。

你的測試套件通過了。你的型別檢查器是綠燈。你發布了。兩小時後，生產環境在某個沒人想到要測試的邊緣案例上拋出了 。 測試能找到錯誤。型別能防止一部分。但兩者都無法證明你的程式完全沒有執行時錯誤。為此，你需要更強大的東西：一種能夠同時對所有可能的執行路徑進行推理、而不需要實際執行程式的方法。…