盡管傳統的斷言可以增加對 Java 代碼所作的檢查次數，但僅用它們，還是有許多檢查無法完成。處理這種情況的方法之一就是使用 時態邏輯。請回憶上個月的文章“ Assertions and temporal logic in Java programming”，時態邏輯有助於提供比程序中的方法更有力的斷言，從而有助於增強用其它方式難以正式表達的不變量。
我們不必費力搜尋去發現有助於防止我們程序出錯的許多有用的不變量。實際上，可以通過使用此類時態邏輯斷言來加大我們消除一些最常見錯誤模式的力度。在本文中，我們將研究一些錯誤模式，使用時態邏輯能會對它們產生最積極的影響。我們將把下列錯誤模式用作示例：
懸掛復合（Dangling Composite）。當您的軟件拋出空指針異常時這個錯誤發生，因為遞歸數據類型的錯誤表示，所以這是個難以診斷的問題。
破壞者數據（Saboteur Data）。這種錯誤在已存儲的數據不能滿足某些句法或語義約束時發生；此時軟件會因為代碼操縱的數據中的錯誤而不是編碼中的錯誤而崩潰。
Split Cleaner。當資源的獲取和釋放按方法邊界一分為二，允許某些控制流不釋放它們本該釋放的資源，其表現形式為洩漏或過早地釋放它們時，這種錯誤發生。
孤線程（Orphaned Thread）。當主線程拋出異常而剩余線程繼續運行，並等待更多輸入到該隊列時，這種錯誤發生；這種錯誤可能導致程序凍結。
臆想實現。當您“實現”了接口，但實際上沒有滿足其預期的語義時，這種錯誤發生。
懸掛復合錯誤模式
懸掛復合錯誤模式包括遞歸數據類型的錯誤表示、將一些類型的基本情況表示為空值而非單獨的類。這樣做會導致難以診斷的 NullPointerException 。
例如，假定您創建了下列“討厭的”數據類型來表示二叉樹：
清單 1. 一些非常糟糕的樹
public class Tree {
public int value;
public Tree left;
public Tree right;
// Leaves are represented as Trees
// with null branches.
public Tree(int _value) {
this.value = _value;
this.left = null;
this.right = null;
}
public Tree(int _value, Tree _left, Tree _right) {
this.value = _value;
this.left = _left;
this.right = _right;
}
}
大家注意，除了作為糟糕的示例，請不要將這個代碼用於任何其它用途！
這段代碼造成了懸掛復合。二叉樹葉子被表示為左右分支都是空值的 Tree。如果我們嘗試向下遞歸這樣的樹，可能很容易引發 NullPointerException
防止這種錯誤模式的最佳方法是：將數據類型的表示重構為 Composite 類層次結構（請在 參考資料一節參閱關於這個主題的文章）。假定您恰好已經完成了這樣的重構，如下所示：
清單 2. 更好的、已重構的樹
abstract class Tree {
public int value;
public Tree(int _value) {
this.value = _value;
}
}
class Leaf extends Tree {
private Leaf(int _value) {
super(_value);
}
}
class Branch extends Tree {
public Tree left;
public Tree right;
public Branch(int _value, Tree _left, Tree _right) {
super(_value);
this.left = _left;
this.right = _right;
}
}
您希望確保其余代碼（或任何外部客戶機代碼）都不會再構造任何舊的懸掛復合：您如何做到這一點呢？
很容易：做一次徹底的編譯。如果您試圖構造 Tree 類的實例，就會得到編譯器錯誤。而且因為 Tree 是抽象的，所以當您試圖編譯新程序時，來自類型檢查器的錯誤將通知您每個應該重構的構造位置。此外，left 和 right 字段被移到 Branches 類這一事實意味著： Tree 類中每條設置這些字段的值的語句也都會引起類型檢查錯誤。
根據這個示例演示，類型檢查器可以成為功能極強大的重構工具。但請考慮一下這種世界末日般的情景：新客戶機程序員可能牢記著構造二叉樹葉的舊的做法，並嘗試通過構造 Branch 類的新實例來構造新葉子，因此給左右分支都傳遞空值。那麼，使用時態邏輯，您可以在該字段上設置“Always”斷言，它將斷言該字段永遠不接收空值：
Always{left != null}
Always{right != null}
當然，我們也可以用在字段上放置類似的普通斷言的方法重構代碼。但是這個過程要麻煩得多。具體來說，我們必須使該字段成為私有的（private），添加一個 setter ，並把代碼中設置該字段的地方重構為調用寫方法（setter）（我們可以在執行這個操作時利用類型檢查器，就象上個示例中一樣）。然後，我們可以在該寫方法（setter）上放一個普通斷言，聲明所設置的值不能為空。
因此，在本例中，您可以根本不用時態邏輯斷言就能完成任務，但會困難得多。讓我們研究一些其它的錯誤模式，對於這些模式時態邏輯能向我們提供了更大的好處。
破壞者數據錯誤模式
破壞者數據錯誤模式在已存儲的數據不能滿足某些句法或語義約束時發生。此類數據會長期休眠，然後在訪問時被激發。
防止這種錯誤模式的最佳方法是：在將數據放置到長期存儲器 之前，對它執行足夠的檢查。但假定您維護一個具有多個客戶機的數據庫，其中有些客戶機不受您控制，所有客戶機都有寫訪問權。您如何防止插入不合適的數據呢？
保護措施的第一級是為所有數據庫訪問（以仲裁器 (Mediator) 形式）提供單個控制點。但是，您還是有可能不能防止惡意（或只是無心的）客戶機突破您的抽象層並通過另外的路徑輸入數據。
有助於快速診斷此類問題的方法之一是在數據庫上放置時態斷言。這些時態斷言可以將希望保存的句法和語義不變量聲明為“Always”斷言：
ForAll x in Employees . Always{Age >= 0}
ForAll x,y in Employees . Always{isMarried(x,y) implies isMarried{y,x}}
etc.
Split Cleaner 錯誤模式
Split Cleaner 錯誤模式資源的獲取和釋放按方法邊界一分為二，允許某些控制流不釋放它們本該釋放的資源時發生。
處理這種錯誤模式的最佳方法是重構。但如果代碼庫很大並且寫得很糟糕，就很難確保已經全面跟蹤了所有可能的執行路徑。
在那種情況下，Split Cleaner 錯誤模式會轉換成另一種形式：我們將嘗試多次釋放資源，而不是一味地不釋放資源。
我們可以做的、有助於把我們從這種可悲的重構嘗試中解脫出來的事情是：在最初獲取該資源的方法中放置一條時態斷言，以達到這樣的效果，如果資源已被釋放，那麼除非它再次被獲取，否則不會被再次釋放。
例如，考慮下列用於打開和關閉文件的糟糕得驚人代碼。
import java.io.*;
class ReaderMaker {
String name;
public ReaderMaker(String _name) {
this.name = _name;
}
FileReader getReader() {
return new FileReader(this.name);
}
...
}
class Client1 {
...
void doSomeWork(ReaderMaker maker) {
FileReader reader = maker.getReader();
...
reader.close();
}
}
當我們完成了對 FileReaders 的使用時，誰負責關閉它？很明顯是客戶機。這是 Split Cleaner 的典型情況。當用不同的方法負責獲得和釋放資源這兩種行為時，就很容易取得資源卻永不釋放。
首先，時態邏輯斷言對於診斷此類錯誤也是有用的。例如，如果我們懷疑一個 Split Cleaner，那麼，可以在獲取資源的方法上放置一個斷言：如果獲取了資源，則最終要釋放它。然後，如果程序執行沒有滿足斷言而終止，將用錯誤消息通知我們。理想情況下，所有資源獲取行為都將首先包括這個斷言，因此一出現 Split Cleaner 就會盡快通知我們。
孤線程錯誤模式
孤線程錯誤模式在多線程程序中某些線程等待已終止的線程時發生。
時態邏輯可以有助於診斷此類錯誤。在每個放置了“wait”以等待其它線程應答的實例中，我們都可以插入一個斷言以使等待最終得到滿足。如果它永遠得不到應答，當程序終止時，我們將得到一條說明情況的錯誤消息：
Always{wait() implies {Sometime{notify()}}}
臆想實現錯誤模式
時態邏輯斷言最直接的應用是在接口上添加可執行文檔，從而在一旦違反這些斷言時就立即捕捉接口的 臆想實現。
例如，考慮我喜歡的接口示例： Stack 。我們可以向這個接口添加非常強有力的斷言，以表達如下所示的意思：
// Once push(x) occurs, top() will return x until a push or a pop occurs.
Always{push(x) implies {{top() == x} until {push(y) || pop()}}
// If the stack is empty, there should be no pops until a push occurs.
Always{isEmpty() implies {{! pop()} until {push(x)}}}
// (if we have a length operation) If the length is n, and a push occurs,
// then next step, the length will be n+1.
Always{{length == n && push(x)} implies {Next{length == n + 1}}}
您明白其意義了吧。
接口中的時態邏輯斷言不但比散文（prose）精確得多，而且，實際上在運行時它們是強制執行的（如果我們運行的代碼包含斷言檢查手段的話）。
把松散的思路串起來
正如我們在本文和前一篇專欄文章中所看到的，因為每個時態邏輯斷言可以對應多個傳統斷言，所以時態邏輯斷言可以輔助您更有力地進行單元測試，因此它們的功能是很強大的。
在本文中，我們展示了如何用時態邏輯斷言對付下列錯誤模式：
懸掛復合。在字段上使用用比較簡單的“Always”斷言來聲明該字段永遠不使用空值。
破壞者數據。在數據庫上使用“Always”斷言來聲明希望在數據庫中保存的句法和語義不變量。
Split Cleaner。在最初獲取資源的方法中使用時態斷言來聲明：如果該資源已被釋放，那麼直到它再次被獲取，才會被再次釋放。此處也可以使用時態斷言作為出錯診斷工具。
孤線程。使用時態斷言來聲明：無論何處，只要在線程上放置了等待其它線程應答的“wait”，則“wait”最終將得到滿足。此外，該技術也可用作出錯診斷工具。
臆想實現。將時態斷言用作接口上附加的可執行文檔，以便在違反斷言時立即捕捉接口的臆想實現。
下一次，我們還將討論更多用來改進您代碼健壯性的方法。尤其是，我們將研究一些激動人心的新工具，以通過研究 JUnit 測試套件，這些新工具能夠 自動地檢測有意放置在您代碼上的斷言。
