Shulou(Shulou.com)06/02 Report--

This article mainly shows you "what are the side effects of using JML to improve Java programs?" the content is simple and clear. I hope it can help you solve your doubts. Let me lead you to study and learn this article "what are the side effects of using JML to improve Java programs?"

Side effect

Recall the post-processing code for the pop () method in snippet 2:

XML:namespace prefix = o ns = "urn:schemas-microsoft-com:Office:office" / >

Ensures

ElementsInQueue.equals ((JMLobjectBag)

Old (elementsInQueue))

.remove (esult) & &

Esult.equals (old (peek ()

Here we say that there is a side effect, that is, when an element is deleted from elementsInQueue. In fact, there may be other side effects. For example, if the value of m_isMinHeap is changed in the concrete implementation of a pop () method, the sorting method is changed from a small top heap to a large top heap. As long as this modification returns the correct result, it does not cause an assertion check exception at run time, but this actually weakens the role of the JML behavior specification. We can strengthen the post condition and do not allow any changes other than modifying the elementsInQueue, please see the following code:

Code break 7 post-conditions for reinforcement

Ensures

ElementsInQueue.equals ((JMLObjectBag)

Old (elementsInQueue))

.remove (esult) & &

Esult.equals (old (peek () &

IsMinimumHeap = = old (isMinimumHeap) & &

Comparator = = old (comparator)

We can see that by adding statements such as x = = old (x), we can eliminate the side effect of changing the variable x. However, there is a problem, if you use this method, each method in its post-condition has to add such a sentence to each variable, which will lead to confusion in the code of conduct. And if we add a member variable to a class, we have to add a sentence to the post-processing specification of all methods of the class, which makes maintenance extremely difficult. JML provides a better solution by introducing assignable statements.

Assignable statement

Using the assignment statement, we can complete the post condition of the pop () method as follows:

Code snippet 8 uses the assignment statement in the behavior specification of the method

/ * @

@ public normal_behavior

@ requires! IsEmpty ()

@ assignable elementsInQueue

@ ensures

@ elementsInQueue.equals ((JMLObjectBag)

@ old (elementsInQueue))

@ .remove (esult) & &

Esult.equals (old (peek ()

@ * /

Object pop () throws NoSuchElementException

Only variables listed in the assignable statement can be modified in the implementation of a method. The assignable statement of the pop () method above means that the value of elementsInQueue can be modified in the implementation of the pop () method, but no other variables, such as isMinimumHeap, comparator, and so on, can be modified. If you change the value of m_isMinHeap in the implementation of the pop () method, an error will occur at compile time. (however, the current JML compiler does not support this, that is, it does not check whether the implementation of the method modifies only the variables specified in the assignable statement. )

Modify a rule

We said earlier that only the variables listed in the assignable statement can be modified in the implementation of a method, which is actually a bit simplified. In fact, the rule allows the method to modify a variable (loc) if any of the following conditions are true:

Loc is explicitly listed in the assignable statement.

The variables listed in the assignable statement depend on loc. (for example, if we declare "assignable isMinimumHeap;", because the model domain isMinimumHeap depends on the specific domain m_isMinHeap, this assignable statement means that the method can modify not only the explicitly declared isMinimumHeap, but also the m_isMinHeap. )

The loc has not been allocated when the method starts execution.

Loc is a local variable of a method or a formal parameter of a method.

The last case allows a method to modify its parameter, even if the parameter does not appear explicitly in the assignable statement. At first glance, this seems to allow a method to pass parameters that allow its caller to modify the value of a variable. For example, there is a method foo (Bar obj) that has a statement obj = anotherBar. However, although this statement modifies the value of obj, it does not affect the caller of foo (), because although both obj point to a Bar object and have the same name, the obj in the foo () method is actually different from the obj in the caller of foo ().

Now let's consider what happens if the method foo (Bar obj) has a statement called obj.x = 17. This will explicitly change the variable in the caller. There is a problem with this. The rules of the assignable statement allow a method to modify the value of an incoming parameter without declaring it in the assignable statement, but it does not allow you to modify the member variables of the parameter, specifically, the value of obj.x. If you want to change the value of obj.x in the foo () method, you must declare in the assignable statement that you can write assignable obj.x;.

Two JML keywords, othing and everything, can be used in an assignable statement. We can use the assignable othing statement to show that a method does not have any side effects; similarly, we can use the assignable everything statement to show that our method can modify the values of all variables. Earlier we used the JML keyword pure, which is equivalent to using assignable othing;.

These are all the contents of this article entitled "what are the side effects of using JML to improve Java programs?" Thank you for reading! I believe we all have a certain understanding, hope to share the content to help you, if you want to learn more knowledge, welcome to follow the industry information channel!

Welcome to subscribe "Shulou Technology Information " to get latest news, interesting things and hot topics in the IT industry, and controls the hottest and latest Internet news, technology news and IT industry trends.