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

　　我們大家同意對(duì) Java 代碼檢查得越多就越好，我們檢查了斷言在測(cè)試新的和改進(jìn)的編程中的用法。雖然傳統(tǒng)斷言可以增加執(zhí)行的檢查次數(shù)，但有許多檢查不能用它們來(lái)執(zhí)行。

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

　　斷言及其特性

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

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

　　常見(jiàn)的斷言特性

　　傳統(tǒng)上，斷言特性分成下面三種類(lèi)型：

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

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

　　可表示為斷言的程序特性

　　這只是可以用傳統(tǒng)斷言語(yǔ)言表示的程序特性類(lèi)型的簡(jiǎn)短列表 ― 所有程序員都希望在代碼中包含的特性：

• 確保任何一次性特性都僅生成一次
• 斷言文檔決不被未授權(quán)的代理程序訪(fǎng)問(wèn)
• 斷言向每個(gè)線(xiàn)程提供運(yùn)行機(jī)會(huì)
• 斷言系統(tǒng)將決不會(huì)使其本身陷入死鎖

　　安全性協(xié)議使用一次性特性(使用過(guò)一次的數(shù)字)生成器來(lái)確保事務(wù)未被用過(guò)。作為安全性中的簡(jiǎn)單概念，確保一旦生成特殊一次性特性，就不再生成它，這一點(diǎn)很重要。另一個(gè)重要的安全性斷言是安全文檔決不被未授權(quán)的代理程序訪(fǎng)問(wèn)。

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

　　基本的非常規(guī)斷言特性

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

• 安全斷言
• 生存斷言

　　安全斷言聲明某些不合需要的系統(tǒng)狀態(tài)將決不在任何環(huán)境下起作用。生存斷言聲明保證最終發(fā)生某些事件 ― 例如，給定的線(xiàn)程將最終被喚醒，而不是永遠(yuǎn)休眠。

　　時(shí)態(tài)邏輯可以幫助產(chǎn)生這些斷言。

　　時(shí)態(tài)邏輯出現(xiàn)在何處

　　這樣的斷言超出普通斷言語(yǔ)言的表示，但可以用形式體系和工具來(lái)表示這種語(yǔ)句。我們將這種形式體系稱(chēng)為 時(shí)態(tài)邏輯。

　　已定義的時(shí)態(tài)邏輯

　　時(shí)態(tài)邏輯是一種 模態(tài)邏輯，用于推理隨時(shí)間而更改的特性。

　　請(qǐng)始終記住，有兩種常規(guī)的時(shí)態(tài)邏輯：

• 把未來(lái)當(dāng)作為事件的線(xiàn)性序列的模型
• 把未來(lái)當(dāng)作為具有各種可能性的樹(shù)型分叉的模型

　　在本文中，我們將只考慮把未來(lái)當(dāng)作為事件的線(xiàn)性序列模型的時(shí)態(tài)邏輯。(“分叉樹(shù)”邏輯非常酷，但它在計(jì)算上很難處理。)

　　通常，時(shí)態(tài)邏輯構(gòu)建于一組更簡(jiǎn)單的原子(小單元)命題之上，如傳統(tǒng)程序斷言。于是，各種模態(tài)操作符都可以應(yīng)用于這些原子斷言以生成更復(fù)雜的斷言。傳統(tǒng)的布爾邏輯操作符(如 與(and) 或 或(or) )可應(yīng)用于這些斷言以生成甚至更復(fù)雜的斷言。新生成的斷言仍可以生成更復(fù)雜的斷言，并且可以無(wú)限地生成下去。

　　時(shí)態(tài)邏輯使用三個(gè)(或四個(gè)，取決于模型)常見(jiàn)的模態(tài)操作符。

　　典型的模態(tài)操作符

　　通常，下列模態(tài)操作符可用于時(shí)態(tài)邏輯：

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

　　當(dāng)應(yīng)用于斷言時(shí)， Always 確保斷言在整個(gè)程序執(zhí)行的剩余部分繼續(xù)保持。

　　從意義上說(shuō)，操作符 Sometime 與 Always 是親戚，但弱得多。當(dāng)應(yīng)用于斷言時(shí)， Sometime 規(guī)定一定要在程序執(zhí)行的今后時(shí)間內(nèi)存在某些斷言可以起作用的時(shí)間點(diǎn)。

　　Until 應(yīng)用于兩個(gè)斷言，它規(guī)定一旦第一個(gè)斷言停止作用，此后，第二個(gè)斷言就必須保持有效。

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

　　清單 1 顯示了一些時(shí)態(tài)邏輯斷言示例：

　　清單 1. 樣本時(shí)態(tài)邏輯斷言

　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

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

　　清單 2. 說(shuō)明多線(xiàn)程的樣本

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

　　可以擴(kuò)展時(shí)態(tài)邏輯。

　　擴(kuò)展語(yǔ)言

　　我們還可以擴(kuò)展時(shí)態(tài)邏輯的語(yǔ)言以包括數(shù)據(jù)庫(kù)中值集合的量詞。例如，我們可以檢查斷言是否始終對(duì)表中的所有值保持有效或者至少對(duì)表中的一個(gè)值保持有效。

　　有了這種級(jí)別的表示，我們可以構(gòu)成非常強(qiáng)大的安全和安全性斷言。例如，考慮顯式代理對(duì)象可以請(qǐng)求訪(fǎng)問(wèn)各種文檔的環(huán)境。我們可以組成清除可以查看各種文檔的代理的斷言。

　　下列斷言保證沒(méi)有一個(gè)代理可以查看文檔，直到他讓明確可以有權(quán)這樣做：

　　清單 3. 說(shuō)明數(shù)據(jù)庫(kù)安全性的樣本

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

　　如何檢查時(shí)態(tài)邏輯

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

　　對(duì)此我要說(shuō)的是：有專(zhuān)門(mén)檢查這些類(lèi)型的斷言的工具。在數(shù)字電路中，在構(gòu)建芯片之前，先靜態(tài)地驗(yàn)證這類(lèi)斷言。

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

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

　　Temporal Rover 包括所有時(shí)態(tài)操作符以及為討論過(guò)去發(fā)生的事件而設(shè)計(jì)的其它操作符。DBRover 可以以數(shù)據(jù)庫(kù)中值量化斷言。不幸的是，這些工具不是免費(fèi)的，但它們提供了 30 天的免費(fèi)試用版本。

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

　　/* TRAssert{ => }

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

　　結(jié)束語(yǔ)

　　這類(lèi)時(shí)態(tài)邏輯可以幫助您將單元測(cè)試提升到更高的程度，因?yàn)槊總€(gè)時(shí)態(tài)邏輯斷言都可以與許多傳統(tǒng)斷言對(duì)應(yīng)。這意味著這些斷言是如此強(qiáng)大，以致可以有力地幫助消除本專(zhuān)欄文章中討論的許多典型的錯(cuò)誤模式。