JML起步--使用JML改進你的Java程序(3)

2019-11-18 13:17:47

字體：大中小

來源：轉載

供稿：網友

　　請大家回憶一下代碼段2中pop()方法的后處理代碼：
　　
　　ensures
　　
　　elementsInQueue.equals(((JMLObjectBag)
　　
　　　　　　　　 /old(elementsInQueue))
　　
　　　　　　　　　　　　　　　 .remove(/result)) &&
　　
　　/result.equals(/old(peek()));
　　
　　這里我們說有一個副作用，那就是在從elementsInQueue刪除一個元素的時候會有副作用。事實上，這里還可能有其他的副作用。比方說，一個pop()方法的具體實現中假如修改了m_isMinHeap的值，那么就把排序方法從一個小頂堆變成了大頂堆。只要這種修改能夠返回正確結果，就不會引起運行期間的斷言檢查異常，可是這個卻事實上削弱了JML行為規范的作用。我們可以加強后置條件，不答應除了修改elementsInQueue以外的任何改變，請看下面的代碼：
　　
　　代碼斷7　　加強的后置條件
　　
　　ensures
　　
　　elementsInQueue.equals(((JMLObjectBag)
　　
　　　　　　　　/old(elementsInQueue))
　　
　　　　　　　　　　　　　　　 .remove(/result)) &&
　　
　　/result.equals(/old(peek())) &&
　　
　　isMinimumHeap == /old(isMinimumHeap) &&
　　
　　comparator == /old(comparator);
　　
　　從中我們可以看出，通過加入形如x == /old(x)的語句，我們可以消除變量x發生改變的副作用?？墒怯幸粋€問題，假如用這種辦法，每一個方法在它的后置條件都要為每一個變量加上這么一句，這樣就會導致行為規范的混亂。而且假如我們給一個類增加一個成員的變量的話，那么我們就得在這個類的所有方法的后處理規范中增加一句，這將讓維護變得異常困難。 JML通過引入assignable語句提供了一種更好地解決方案。
　　
　　assignable 語句
　　使用assignable語句，我們可以這樣完成pop()方法的后置條件：
　　
　　代碼段8　　在方法的行為規范中使用assignable語句
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 requires ! isEmpty();
　　
　　　 @　 assignable elementsInQueue;
　　
　　　 @　 ensures
　　
　　　 @　　 elementsInQueue.equals(((JMLObjectBag)
　　
　　　 @　　　　　/old(elementsInQueue))
　　
　　　 @　　　　　　　　　　　　.remove(/result)) &&
　　
　　　 @　　 /result.equals(/old(peek()));
　　
　　　 @*/
　　
　　Object pop() throws NoSUChElementException;
　　
　　只有在assignable語句中列出的變量才能在一個方法的實現中修改。上面pop()方法的assignable語句的意思是在pop()方法的實現中可以修改elementsInQueue的值，除此之外的其他變量，比如isMinimumHeap、comparator等等都不可以修改。假如你在pop()方法的實現中修改了m_isMinHeap的值，那么編譯的時候就會產生一個錯誤。（不過當前的JML編譯器尚沒有支持這個，也就是沒有檢查在方法的實現中，是否只修改在assignable語句中指定的變量。）
　　
　　修改規則
　　我們前面說只有在assignable語句中列出的變量才能在一個方法的實現中修改，這其實是有點簡化的說法。事實上，假如以下任意一個條件是 true，該規則就答應方法修改一個變量（loc）：
　　
　　assignable語句中顯式列出loc 。
　　assignable語句中列出的變量依靠于loc。（比如說假如我們聲明“assignable isMinimumHeap;” ，因為模型域isMinimumHeap依靠于具體域m_isMinHeap，所以該 assignable語句意味著方法不僅可以修改顯式聲明的isMinimumHeap，而且還能修改m_isMinHeap。）
　　方法開始執行時loc尚沒有分配。
　　loc 是方法的局部變量或者是方法的形式參數。
　　最后一種情況答應一個方法修改它的參數，即使這個參數沒有顯式地出現在assignable語句中。粗略一看，這個似乎答應一個方法通過參數傳遞答應它的調用者修改變量的值。比方說，有一個方法foo(Bar obj)，它里面有一個語句obj = anotherBar。不過雖然這個語句修改了obj的值，卻不會影響到foo()的調用者，因為雖然這兩個obj都是指向一個Bar對象，而且具有一樣的名字，foo()方法中的此obj實際上與foo()的調用者中的彼obj是不同的（譯者注：關于這一點，請參考java中索引與對象的概念）。
　　
　　現在我們考慮假如方法foo(Bar obj)里面有一個語句obj.x = 17會怎么樣？這個將顯式地改變調用者中的變量。這是有問題的。assignable 語句的規則答應一個方法不需要在assignable 語句中聲明就可以修改傳入參數的值，不過它并不答應修改參數的成員變量，具體在這里來說，就是不答應修改obj.x的值。假如你希望在foo()方法中修改obj.x的值，你就必須在assignable 語句中聲明，你可以寫assignable obj.x; 。
　　
　　assignable 語句中可以使用兩個JML要害字，/nothing和/everything。我們可以通過assignable /nothing 語句來表明一個方法沒有任何副作用；同樣，我們可以通過assignable /everything語句來表明我們的方法可以修改一切變量的值。早先我們使用了一個JML要害字pure，它就等同于使用assignable /nothing; 。

上一篇：JML起步--使用JML改進你的Java程序(4)

下一篇：Model View Controller 與 Observer