雖然傳統斷言可以增加對 Java 代碼執行的檢查次數，但有許多檢查不能用它們來執行。彌補這一缺陷的方法是使用“時態邏輯”，它是一種用于描述程序狀態如何隨時間而更改的形式體系。在本文中，Eric Allen 將討論斷言，介紹時態邏輯并描述用于處理程序中時態邏輯斷言的工具。

　　我們大家同意對 Java 代碼檢查得越多就越好，我們檢查了斷言在測試新的和改進的編程中的用法。雖然傳統斷言可以增加執行的檢查次數，但有許多檢查不能用它們來執行。

　　然而，有一個方法可以彌補斷言留下的檢查缺口。那就是使用 時態邏輯。時態邏輯是用于描述程序狀態如何隨時間而更改的形式體系。讓我們討論一下斷言及其特性，以及時態邏輯是如何適合檢查的。然后，我們將研究用于處理時態邏輯斷言的工具。

　　斷言及其特性

　　除了類型檢查和單元測試外，斷言還提供了一種確定各種特性是否在程序中得到維護的極好方法。

　　讓我們快速瀏覽三種類型常見的斷言特性(雖然是常見的，但它們沒有提供我們所需的完整范圍)，將它們與可以用傳統斷言語言表示的程序特性的類型進行比較，并檢查多線程上下文所必需的，但不可能表示成常規斷言的斷言特性。我們還將提供一些代碼示例。

　　常見的斷言特性

　　傳統上，斷言特性分成下面三種類型：

• 代碼塊執行之前特性所持有的條件前斷言。
• 代碼塊執行之后特性所持有的條件后斷言。
• 代碼塊執行之前和之后特性所持有的不變斷言。

　　與這些典型形式的斷言一樣有用，它們不太會有我們希望能在程序中持有的所有特性范圍。讓我們看一下典型的用斷言表示的程序特性。

　　可表示為斷言的程序特性

　　這只是可以用傳統斷言語言表示的程序特性類型的簡短列表 ― 所有程序員都希望在代碼中包含的特性：

• 確保任何一次性特性都僅生成一次
• 斷言文檔決不被未授權的代理程序訪問
• 斷言向每個線程提供運行機會
• 斷言系統將決不會使其本身陷入死鎖

　　安全性協議使用一次性特性(使用過一次的數字)生成器來確保事務未被用過。作為安全性中的簡單概念，確保一旦生成特殊一次性特性，就不再生成它，這一點很重要。另一個重要的安全性斷言是安全文檔決不被未授權的代理程序訪問。

　　在多線程代碼中，我們希望斷言每個線程最終都會有運行機會。我們還希望確保系統決不會使其本身陷入 死鎖狀態(即在兩個或多個線程可以繼續處理之前，它們正在彼此等待提供資源)。

　　基本的非常規斷言特性

　　下面是我們希望獲得的(通常想要在多線程代碼環境中獲得的)兩種非常有用的特性類型，不可能僅用常規斷言來表示它們：

• 安全斷言
• 生存斷言

　　安全斷言聲明某些不合需要的系統狀態將決不在任何環境下起作用。生存斷言聲明保證最終發生某些事件 ― 例如，給定的線程將最終被喚醒，而不是永遠休眠。

　　時態邏輯可以幫助產生這些斷言。

　　時態邏輯出現在何處

　　這樣的斷言超出普通斷言語言的表示，但可以用形式體系和工具來表示這種語句。我們將這種形式體系稱為 時態邏輯。

　　已定義的時態邏輯

　　時態邏輯是一種 模態邏輯，用于推理隨時間而更改的特性。

　　請始終記住，有兩種常規的時態邏輯：

• 把未來當作為事件的線性序列的模型
• 把未來當作為具有各種可能性的樹型分叉的模型

　　在本文中，我們將只考慮把未來當作為事件的線性序列模型的時態邏輯。(“分叉樹”邏輯非?？?，但它在計算上很難處理。)

　　通常，時態邏輯構建于一組更簡單的原子(小單元)命題之上，如傳統程序斷言。于是，各種模態操作符都可以應用于這些原子斷言以生成更復雜的斷言。傳統的布爾邏輯操作符(如 與(and) 或 或(or) )可應用于這些斷言以生成甚至更復雜的斷言。新生成的斷言仍可以生成更復雜的斷言，并且可以無限地生成下去。

　　時態邏輯使用三個(或四個，取決于模型)常見的模態操作符。

　　典型的模態操作符

　　通常，下列模態操作符可用于時態邏輯：

• Always
• Sometime
• Until
• Next (特殊情況)

　　當應用于斷言時， Always 確保斷言在整個程序執行的剩余部分繼續保持。

　　從意義上說，操作符 Sometime 與 Always 是親戚，但弱得多。當應用于斷言時， Sometime 規定一定要在程序執行的今后時間內存在某些斷言可以起作用的時間點。

　　Until 應用于兩個斷言，它規定一旦第一個斷言停止作用，此后，第二個斷言就必須保持有效。

　　當時間可以是由一系列不連續步驟(比如，程序執行期間)組成的模型時，您有時候會看到 Next 操作符被添加到這個著名的列表中。當 Next應用于斷言時，它規定斷言在“下一個”步驟中保持有效。當然，僅當我們將時間分割成不連續步驟時，這才有意義。

　　清單 1 顯示了一些時態邏輯斷言示例：

　　清單 1. 樣本時態邏輯斷言

　Always x != 0
　　Sometime x == 0
　　{x == y} implies {Next {x == y + 1}}
　　{x == y} Until {y == 0}
　　{x == 0} implies {Next {Always {x != 0}}} // x is zero only once
　　Sometime {! this.isInterrupted()} // this thread is not interrupted forever

　　下面是兩個斷言它們從不死鎖的線程的示例斷言。(注：布爾方法 isWaitingOn 用于檢查一個線程是否被另一個線程執行的任務掛起。)

　　清單 2. 說明多線程的樣本

　Always {x.isWaitingOn(y) implies {! y.isWaitingOn(x)}}

　　可以擴展時態邏輯。

　　擴展語言

　　我們還可以擴展時態邏輯的語言以包括數據庫中值集合的量詞。例如，我們可以檢查斷言是否始終對表中的所有值保持有效或者至少對表中的一個值保持有效。

　　有了這種級別的表示，我們可以構成非常強大的安全和安全性斷言。例如，考慮顯式代理對象可以請求訪問各種文檔的環境。我們可以組成清除可以查看各種文檔的代理的斷言。

　　下列斷言保證沒有一個代理可以查看文檔，直到他讓明確可以有權這樣做：

　　清單 3. 說明數據庫安全性的樣本

　　ForAll agents in AgentPool
　　{ForAll document in TopSecretDocumentPool
　　{{! agent.canView(document)} Until {agent.hasClearanceFor(document)}}}

　　如何檢查時態邏輯

　　現在，您可能會提出異議：“喔!我可以 講所有這些事情真是太棒了，但我無法檢查我所講的是否正確，那么問題在哪里呢?!”

　　對此我要說的是：有專門檢查這些類型的斷言的工具。在數字電路中，在構建芯片之前，先靜態地驗證這類斷言。

　　在軟件中，我們 靜態檢查這種斷言的能力是微不足道的，但存在用于檢查這些斷言在程序的特殊運行(例如，單元測試的運行)期間是否保持有效的品質工具。這樣的斷言可以幫助您將單元測試提升到很高的程度;每個時態邏輯斷言都可以與無數的傳統斷言對應(并且只是在傳統斷言完全可以用來表示斷言的情況下)。

　　Time Rover Inc. 的 Temporal Rover 是一種用于處理 Java 程序中時態邏輯斷言并根據斷言生成有效 Java 代碼的工具。該公司還提供用于數據庫表的工具 DBRover。

　　Temporal Rover 包括所有時態操作符以及為討論過去發生的事件而設計的其它操作符。DBRover 可以以數據庫中值量化斷言。不幸的是，這些工具不是免費的，但它們提供了 30 天的免費試用版本。

　　與 JUnit 中的斷言相似，Temporal Rover/DBRover 斷言為程序員提供了在斷言失敗時打印診斷消息的選項。實際上，Temporal Rover 斷言的語法與我在上面示例中使用的語法相同，其中，模態操作符采用的斷言用花括號括起。然后，這些斷言被傳遞到具有下列語法的 TRAssert 函數(Temporal Rover Assert)：

　　/* TRAssert{ => }

　　是在斷言無法保持有效時顯示的。這樣， TRAssert 語句就可以嵌入到有效的 Java 程序，并且這些程序仍可以不用 Temporal Rover 進行編譯(當然，不用 Temporal Rover 進行編譯可以使斷言免受任何影響)。

　　結束語

　　這類時態邏輯可以幫助您將單元測試提升到更高的程度，因為每個時態邏輯斷言都可以與許多傳統斷言對應。這意味著這些斷言是如此強大，以致可以有力地幫助消除本專欄文章中討論的許多典型的錯誤模式。