assignable語句

使用assignable語句，我們可以這樣完成pop()方法的后置條件：

代碼段8 在方法的行為規(guī)范中使用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語句中列出的變量才能在一個方法的實現(xiàn)中修改。上面pop()方法的assignable語句的意思是在pop()方法的實現(xiàn)中可以修改elementsInQueue的值，除此之外的其他變量，比如isMinimumHeap、comparator等等都不可以修改。如果你在pop()方法的實現(xiàn)中修改了m_isMinHeap的值，那么編譯的時候就會產(chǎn)生一個錯誤。（不過當(dāng)前的JML編譯器尚沒有支持這個，也就是沒有檢查在方法的實現(xiàn)中，是否只修改在assignable語句中指定的變量。）

修改規(guī)則

我們前面說只有在assignable語句中列出的變量才能在一個方法的實現(xiàn)中修改，這其實是有點簡化的說法。事實上，如果以下任意一個條件是 true，該規(guī)則就允許方法修改一個變量（loc）：

• assignable語句中顯式列出loc 。

• assignable語句中列出的變量依賴于loc。（比如說如果我們聲明“assignable isMinimumHeap;” ，因為模型域isMinimumHeap依賴于具體域m_isMinHeap，所以該 assignable語句意味著方法不僅可以修改顯式聲明的isMinimumHeap，而且還能修改m_isMinHeap。）

• 方法開始執(zhí)行時loc尚沒有分配。

• loc 是方法的局部變量或者是方法的形式參數(shù)。

最后一種情況允許一個方法修改它的參數(shù)，即使這個參數(shù)沒有顯式地出現(xiàn)在assignable語句中。粗略一看，這個好像允許一個方法通過參數(shù)傳遞允許它的調(diào)用者修改變量的值。比方說，有一個方法foo(Bar obj)，它里面有一個語句obj = anotherBar。不過雖然這個語句修改了obj的值，卻不會影響到foo()的調(diào)用者，因為雖然這兩個obj都是指向一個Bar對象，而且具有一樣的名字，foo()方法中的此obj實際上與foo()的調(diào)用者中的彼obj是不同的（譯者注：關(guān)于這一點，請參考Java中索引與對象的概念）。

現(xiàn)在我們考慮如果方法foo(Bar obj)里面有一個語句obj.x = 17會怎么樣？這個將顯式地改變調(diào)用者中的變量。這是有問題的。assignable 語句的規(guī)則允許一個方法不需要在assignable 語句中聲明就可以修改傳入?yún)?shù)的值，不過它并不允許修改參數(shù)的成員變量，具體在這里來說，就是不允許修改obj.x的值。如果你希望在foo()方法中修改obj.x的值，你就必須在assignable 語句中聲明，你可以寫assignable obj.x; 。

assignable 語句中可以使用兩個JML關(guān)鍵字， othing和everything。 我們可以通過assignable othing 語句來表明一個方法沒有任何副作用；同樣，我們可以通過assignable everything語句來表明我們的方法可以修改一切變量的值。早先我們使用了一個JML關(guān)鍵字pure，它就等同于使用assignable othing; 。