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

2019-11-18 14:02:35

字體：大中小

來源：轉載

供稿：網友

　　來自:http://www-106.ibm.com/ 作者:Joe Verzulli

副作用

請大家回憶一下代碼段2中pop()方法的后處理代碼：

ensures

elementsInQueue.equals(((JMLObjectBag)

old(elementsInQueue))

.remove(esult)) &&

esult.equals(old(peek()));

這里我們說有一個副作用，那就是在從elementsInQueue刪除一個元素的時候會有副作用。事實上，這里還可能有其他的副作用。比方說，一個pop()方法的具體實現中假如修改了m_isMinHeap的值，那么就把排序方法從一個小頂堆變成了大頂堆。只要這種修改能夠返回正確結果，就不會引起運行期間的斷言檢查異常，可是這個卻事實上削弱了JML行為規范的作用。我們可以加強后置條件，不答應除了修改elementsInQueue以外的任何改變，請看下面的代碼：

代碼斷7 加強的后置條件

ensures

elementsInQueue.equals(((JMLObjectBag)

old(elementsInQueue))

.remove(esult)) &&

esult.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(esult)) &&

@ esult.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要害字，othing和everything。我們可以通過assignable othing 語句來表明一個方法沒有任何副作用；同樣，我們可以通過assignable everything語句來表明我們的方法可以修改一切變量的值。早先我們使用了一個JML要害字pure，它就等同于使用assignable othing; 。

上一篇：JBuilder9＋weblogic7.0完全攻略

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