side effect
Please recall the post-processing code of the POP () method in the code segment 2:
EnsuRES
Elementsinqueue.equals ((JMLObjectbag)
/ OLD (Elementsinqueue))
.remove (/ result) &&
/Result.equals (/ OLD (PEEK ()));
Here we say there is a side effect, that is, there will be side effects when deleting an element from ElementSinQueue. In fact, there may be other side effects here. For example, if a POP () method is modified, if the value of m_isminheap is modified, the sorting method becomes a large top heap. As long as this modification can return the correct result, it will not cause assertion inspections during operation, but this is in fact to weaken the role of JML behavioral specifications. We can strengthen the back conditions, do not allow any changes other than modifying ElementSINQUEUE, please see the following code:
Code break 7 enhanced back conditions
EnsuRES
Elementsinqueue.equals ((JMLObjectbag)
/ OLD (Elementsinqueue))
.remove (/ result) &&
/Result.equals (/ OLD (PEEK ()) &&
IsminimumHeap == / OLD (isminimumHeap) &&&&&&&&&&
Comparator == / OLD (Compare);
From this we can see that we can eliminate the side effects of variable X by adding a statement such as x = / OLD (X). However, there is a problem, if this method is used, each method is to add such a variable in its back conditions, which will lead to confusion of behavioral specifications. And if we add a variable that adds a member of a member, then we have to add a sentence in the post-processing specification of all the methods of this class, which will make maintenance unusually difficult. JML provides a better solution by introducing an Assignable statement.
Assignable statement
Using the Assignable statement, we can complete the back conditions of the POP () method:
The code segment 8 uses the assignable statement in the behavioral specification method
/ * @
@ public normal_behavior
@ Requires! ISempty ();
@ Assignable elementsinqueue;
@ Ensures
@ Elementsinqueue.equals ((JMLObjectbag)
@ / OLD (ElementSINQUEUE))
@ .Remove (/ result) &&
@ /Result.equals (/ OLD (PEEK ()));
@ * /
Object pop () throws nosuchelementexception;
Only variables listed in the assignable statement can be modified in a way. The assignable statement of the above POP () method means modifying the value of ElementSinQueue in the implementation of the POP () method, in addition to other variables, such as ISMINIMUMHEAP, COURATOR, etc. cannot be modified. If you modify the value of m_isminheap in the implementation of the POP () method, you will generate an error when compiling. (However, the current JML compiler has not yet supported this, which is not checked in the implementation of the method, whether it only modifies the variables specified in the Assignable statement.)
Modifying rules We have said that only the variables listed in the assignable statement can be modified in a method's implementation, which is actually a bit simplicity. In fact, if any of the following conditions is true, this rule allows the method to modify a variable (LOC):
Explicitly listing the LOC in the Assignable statement.
The variables listed in the assignable statement depends on the LOC. (For example, if we declare "assignable isminimumheap, because the model domain isminimumheap depends on the specific domain m_isminheap, the Assignable statement means that the method can not only modify the explicit declared ISMINIMUMHEAP, but also modify m_isminheap.)
The method is not allocated when the method starts.
LOC is a local variable of the method or the formal parameters of the method.
The last case allows a method to modify its parameters, even if this parameter does not explicitly appear in the Assignable statement. A rough look, this seems to allow a method to pass the parameters to allow its caller to modify the value of the variable. For example, there is a method foo (bar obj), there is an Obj = anotherbar in it. However, although this statement modifies the value of OBJ, it does not affect the invager of Foo (), because although these two OBJ are pointing to a BAR object, and has the same name, this OBJ in the foo () method actually The other Obj in the caller of foo () is different (the translator's note: About this, please refer to the concept of indexing and objects in Java).
Now we consider if there is an obj.x = 17 in the method foo (bar obj)? This will explicitly change the variables in the caller. This is problematic. The rule of Assignable statement allows a method to modify the value of the incoming parameters without the declaration of the assignable statement, but it does not allow the member variables of the parameters, which is not allowed to modify the value of Obj.x. If you want to modify the value of Obj.x in the foo () method, you must declare in the assignable statement, you can write Assignable Obj.x;.
Two JML keywords, / nothing, and / everything can be used in the Assignable statement. We can use the assignable / nothing statement to indicate that there is no side effects; the same, we can use the assignable / everything statement to indicate that our method can modify the value of all variables. We use a JML keyword Pure, which is equivalent to using assignable / nothing; Please refer to: http://www.9cbs.net/develop/read_article.asp?id=19198 JML start --- Use JML to improve your Java program (1) http://www.9cbs.net/develop /read_article.asp?id=19199 JML start --- Use JML to improve your Java program (2) http://www.9cbs.net/develop/read_article.asp?id=19202 JML start --- use JML improvement Your Java program (4)
