內(nèi)容: 來(lái)自:http://www-106.ibm.com/ 作者:Joe Verzulli 副作用請(qǐng)大家回憶一下代碼段2中pop()方法的后處理代碼： ensureselementsInQueue.equals(((JMLObjectBag) old(elementsInQueue)) .remove(result)) &&result.equals(old(peek())); 這里我們說(shuō)有一個(gè)副作用，那就是在從elementsInQueue刪除一個(gè)元素的時(shí)候會(huì)有副作用。事實(shí)上，這里還可能有其他的副作用。比方說(shuō)，一個(gè)pop()方法的具體實(shí)現(xiàn)中如果修改了m_isMinHeap的值，那么就把排序方法從一個(gè)小頂堆變成了大頂堆。只要這種修改能夠返回正確結(jié)果，就不會(huì)引起運(yùn)行期間的斷言檢查異常，可是這個(gè)卻事實(shí)上削弱了JML行為規(guī)范的作用。我們可以加強(qiáng)后置條件，不允許除了修改elementsInQueue以外的任何改變，請(qǐng)看下面的代碼： 代碼斷7 加強(qiáng)的后置條件 ensureselementsInQueue.equals(((JMLObjectBag) old(elementsInQueue)) .remove(result)) &&result.equals(old(peek())) &&isMinimumHeap == old(isMinimumHeap) &&comparator == old(comparator); 從中我們可以看出，通過(guò)加入形如x == old(x)的語(yǔ)句，我們可以消除變量x發(fā)生改變的副作用。可是有一個(gè)問(wèn)題，如果用這種辦法，每一個(gè)方法在它的后置條件都要為每一個(gè)變量加上這么一句，這樣就會(huì)導(dǎo)致行為規(guī)范的混亂。而且如果我們給一個(gè)類(lèi)增加一個(gè)成員的變量的話，那么我們就得在這個(gè)類(lèi)的所有方法的后處理規(guī)范中增加一句，這將讓維護(hù)變得異常困難。 JML通過(guò)引入assignable語(yǔ)句提供了一種更好地解決方案。 assignable 語(yǔ)句使用assignable語(yǔ)句，我們可以這樣完成pop()方法的后置條件： 代碼段8 在方法的行為規(guī)范中使用assignable語(yǔ)句 /*@ @ public normal_behavior @ requires ! isEmpty(); @ assignable elementsInQueue; @ ensures @ elementsInQueue.equals(((JMLObjectBag) @ old(elementsInQueue)) @ .remove(result)) && @ result.equals(old(peek())); @*/Object pop() throws NoSuchElementException; 只有在assignable語(yǔ)句中列出的變量才能在一個(gè)方法的實(shí)現(xiàn)中修改。上面pop()方法的assignable語(yǔ)句的意思是在pop()方法的實(shí)現(xiàn)中可以修改elementsInQueue的值，除此之外的其他變量，比如isMinimumHeap、comparator等等都不可以修改。如果你在pop()方法的實(shí)現(xiàn)中修改了m_isMinHeap的值，那么編譯的時(shí)候就會(huì)產(chǎn)生一個(gè)錯(cuò)誤。（不過(guò)當(dāng)前的JML編譯器尚沒(méi)有支持這個(gè)，也就是沒(méi)有檢查在方法的實(shí)現(xiàn)中，是否只修改在assignable語(yǔ)句中指定的變量。） 修改規(guī)則我們前面說(shuō)只有在assignable語(yǔ)句中列出的變量才能在一個(gè)方法的實(shí)現(xiàn)中修改，這其實(shí)是有點(diǎn)簡(jiǎn)化的說(shuō)法。事實(shí)上，如果以下任意一個(gè)條件是 true，該規(guī)則就允許方法修改一個(gè)變量（loc）：assignable語(yǔ)句中顯式列出loc 。 assignable語(yǔ)句中列出的變量依賴(lài)于loc。（比如說(shuō)如果我們聲明“assignable isMinimumHeap; ，因?yàn)槟Ｐ陀騣sMinimumHeap依賴(lài)于具體域m_isMinHeap，所以該 assignable語(yǔ)句意味著方法不僅可以修改顯式聲明的isMinimumHeap，而且還能修改m_isMinHeap。） 方法開(kāi)始執(zhí)行時(shí)loc尚沒(méi)有分配。 loc 是方法的局部變量或者是方法的形式參數(shù)。最后一種情況允許一個(gè)方法修改它的參數(shù)，即使這個(gè)參數(shù)沒(méi)有顯式地出現(xiàn)在assignable語(yǔ)句中。粗略一看，這個(gè)好像允許一個(gè)方法通過(guò)參數(shù)傳遞允許它的調(diào)用者修改變量的值。比方說(shuō)，有一個(gè)方法foo(Bar obj)，它里面有一個(gè)語(yǔ)句obj = anotherBar。不過(guò)雖然這個(gè)語(yǔ)句修改了obj的值，卻不會(huì)影響到foo()的調(diào)用者，因?yàn)殡m然這兩個(gè)obj都是指向一個(gè)Bar對(duì)象，而且具有一樣的名字，foo()方法中的此obj實(shí)際上與foo()的調(diào)用者中的彼obj是不同的（譯者注：關(guān)于這一點(diǎn)，請(qǐng)參考Java中索引與對(duì)象的概念）。 現(xiàn)在我們考慮如果方法foo(Bar obj)里面有一個(gè)語(yǔ)句obj.x = 17會(huì)怎么樣？這個(gè)將顯式地改變調(diào)用者中的變量。這是有問(wèn)題的。assignable 語(yǔ)句的規(guī)則允許一個(gè)方法不需要在assignable 語(yǔ)句中聲明就可以修改傳入?yún)?shù)的值，不過(guò)它并不允許修改參數(shù)的成員變量，具體在這里來(lái)說(shuō)，就是不允許修改obj.x的值。如果你希望在foo()方法中修改obj.x的值，你就必須在assignable 語(yǔ)句中聲明，你可以寫(xiě)assignable obj.x; 。 assignable 語(yǔ)句中可以使用兩個(gè)JML關(guān)鍵字，nothing和everything。 我們可以通過(guò)assignable nothing 語(yǔ)句來(lái)表明一個(gè)方法沒(méi)有任何副作用；同樣，我們可以通過(guò)assignable everything語(yǔ)句來(lái)表明我們的方法可以修改一切變量的值。早先我們使用了一個(gè)JML關(guān)鍵字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