內容: 來自:http://www-106.ibm.com/ 作者:Joe Verzulli 副作用請大家回憶一下代碼段2中pop()方法的后處理代碼： ensureselementsInQueue.equals(((JMLObjectBag) old(elementsInQueue)) .remove(result)) &&result.equals(old(peek())); 這里我們說有一個副作用，那就是在從elementsInQueue刪除一個元素的時候會有副作用。事實上，這里還可能有其他的副作用。比方說，一個pop()方法的具體實現中如果修改了m_isMinHeap的值，那么就把排序方法從一個小頂堆變成了大頂堆。只要這種修改能夠返回正確結果，就不會引起運行期間的斷言檢查異常，可是這個卻事實上削弱了JML行為規范的作用。我們可以加強后置條件，不允許除了修改elementsInQueue以外的任何改變，請看下面的代碼： 代碼斷7 加強的后置條件 ensureselementsInQueue.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; 。 Java, java, J2SE, j2se, J2EE, j2ee, J2ME, j2me, ejb, ejb3, JBOSS, jboss, spring, hibernate, jdo, struts, webwork, ajax, AJAX, mysql, MySQL, Oracle, Weblogic, Websphere, scjp, scjd