Java 代碼診斷：用時態邏輯斷言消滅頑固錯誤模式

為何傳統斷言不夠用？

傳統斷言只能檢查「當下」的狀態，無法表達「隨時間演變」的不變量。時態邏輯引入 Always、Sometime、Next、Until 等算子，能精確描述系統在執行軌跡上的屬性，從而捕捉常規單元測試難以覆蓋的深層錯誤模式。

五大經典錯誤模式與時態邏輯對策

1. 懸掛復合——遞歸數據結構的空指針陷阱

將樹葉表示為左右子節點為 null 的節點，極易在遞歸遍歷時觸發 NPE。重構為 Composite 模式（Leaf/Branch 分離）後，在 Branch 的 left/right 字段加上 Always{left != null} 斷言，編譯期即可阻斷錯誤構造。

2. 破壞者數據——長期潛伏的髒數據

數據庫中違反業務約束的數據（如年齡為負、婚姻關係非對稱）可能由不可控客戶端寫入。在關鍵表上聲明 ForAll x in Employees . Always{Age >= 0}、Always{isMarried(x,y) implies isMarried(y,x)}，運行時即可快速定位違規數據源。

3. Split Cleaner——資源獲取釋放分離導致的洩漏

當打開文件與關閉文件分散在不同方法，控制流極易導致資源未釋放或重複釋放。在獲取資源處放置斷言：Always{acquired implies (Released until Reacquired)}，可強制檢測釋放邏輯缺失。

4. 孤線程——主線程異常退出而工作線程永久等待

在每個 wait() 處斷言 Always{wait() implies Sometime{notify()}}，若程序終止前等待未被喚醒，將報錯提示潛在死鎖。

5. 臆想實現——接口簽名符合但語義違背

為 Stack 接口添加強時態契約：

Always{push(x) implies {{top() == x} until {push(y) || pop()}}}
Always{isEmpty() implies {{!pop()} until {push(x)}}}
Always{{length == n && push(x)} implies {Next{length == n+1}}}

任何違背 LIFO 語義的實現（如誤用 Queue）在運行時即會被攔截。

時態邏輯斷言的工程價值

每條時態斷言等價於多條傳統斷言的組合，卻更簡潔、更精準。它們不僅是文檔，更是可執行的運行時守衛。結合自動化斷言檢測工具（如 JUnit 衍生框架），可構建「自我驗證」的代碼庫。下一期將探討如何自動挖掘代碼中隱含的斷言。