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

Editor to share with you the use of JML to improve the Java program quantifier example analysis, I believe that most people do not know much about it, so share this article for your reference, I hope you will learn a lot after reading this article, let's go to know it!

Quantification (translator's note): the meaning of the quantifier here is similar to that of the logical quantifier, rather than the quantifier understood in the general sense. ) XML:namespace prefix = o ns = "urn:schemas-microsoft-com:Office:office" / >

In the behavior specification of the pop () method above, we say that its return value is equal to the return value of the peek () method, but we do not see the specification for the peek () method. For the behavior specification of the peek () method in PriorityQueue, see the following code:

The behavior specification of the peek () method in code snippet 3 PriorityQueue

/ * @

@ public normal_behavior

@ requires! IsEmpty ()

@ ensures elementsInQueue.has (esult)

@ * /

/ * @ pure @ * / object peek () throws NoSuchElementException

The JML tag requires that the peek () method be called only if there is at least one element in the queue, and that the return value of the method must be within the elementsInQueue, that is, it must be an element in the queue.

The comment / * @ pure @ * / indicates that the peek () method is a pure method (pure method), which is a method with no side effects. Only pure methods are allowed for assertion validation in JML, so we declare peek () as a pure method so that we can use the peek () method in the post-condition of the pop () method. You must be wondering why JML only allows assertion confirmation using pure methods. The problem is that if JML allows the use of impure methods for assertion confirmation, we will write a code of behavior with side effects without paying attention. For example, there may be a situation in which our code is correct after the assertion confirmation is turned on, but if the assertion confirmation is disabled, our code will not run, or there may be an error. Of course not! Later, we will further discuss the issue of side effects.

About inheritance

Unlike j2se1.4 interrupts, JML behavioral specifications can be inherited by subclasses (including subinterfaces) or by classes that implement interfaces. The JML keyword also indicates that the currently defined behavior specification works with the behavior specification defined in the ancestor class or the implemented interface. Therefore, the behavior specification of the peek () method defined in the PriorityQueue interface also applies to the peek () method in the BinaryHeap class. This means that although it is not clearly defined in the behavior specification of BinaryHeap.peek (), the return value of BinaryHeap.peek () must also be in elementsInQueue.

Big top heap and small top heap are concepts in the data structure that represent different implementations of heap sorting methods, respectively. Heap sorting is a method of sorting by adjusting the binary tree. )

One obvious missing piece of the behavior specification we defined for peek () above is that the element it returns is not required to have the highest priority at all. Obviously, JCCC's PriorityQueue interface can be used for both large and small top heaps. The performance of the large top heap is different from that of the small top heap. The element with the highest priority in the small top heap has the lowest value, while the element with the highest priority in the large top heap has the highest value. Because PriorityQueue does not know whether it is being used for large or small top heap sorting, the specification that specifies which element to return must be defined in the class that implements the PriorityQueue interface.

In JCCC, the class BinaryHeap implements the PriorityQueue interface. BinaryHeap allows its client code to specify the sorting scheme in the constructor with one parameter, that is, whether to sort by a large top heap or a small top heap. We use a boolean model variable isMinimumHeap to determine whether the BinaryHeap is sorted by a large top heap or a small top heap. The following example is the behavior specification defined by BinaryHeap for the peek () method using isMinimumHeap:

Code snippet 4 behavior specification for the peek () method in the BinaryHeap class

/ * @

@ also

@ public normal_behavior

@ requires! IsEmpty ()

@ ensures

@ (isMinimumHeap = = >

@ (forall Object obj

@ elementsInQueue.has (obj)

@ compareObjects (esult, obj)

@

@ (forall Object obj

@ elementsInQueue.has (obj)

@ compareObjects (esult, obj)

@ > = 0))

@ * /

Public Object peek () throws NoSuchElementException

Use quantifiers

The post condition in snippet 4 above consists of two parts, one for the big top heap and the other for the small top heap. The "= >" symbol means inclusion. X = = > y if and only if y is true or x is false. For small top heap sorting, the code listed below applies:

(forall Object obj

ElementsInQueue.has (obj)

CompareObjects (esult, obj)

@ (esult = = ((Comparable) a) .compareto (b)) & &

@ (comparator! = null) = = >

@ (esult = = comparator.compare (a, b))

@

@ public pure model int compareObjects (Object a, Object b)

@ {

@ if (m_comparator = = null)

@ return ((Comparable) a) .compareto (b)

@ else

@ return m_comparator.compare (a, b)

@}

@ * /

Another keyword model is used in the definition of the compareObjects method, which means that the compareObjects method is a model method. Model methods are JML methods that can only be used in behavioral specifications. Model methods are defined in comments in Java, so regular Java code cannot be used.

If the client code of the BinaryHeap class specifies a special Comparator for comparison, m_comparator points to that Comparator, otherwise the value of m_comparator is null. The compareObjects () method checks the value of m_comparator and then uses the appropriate method to compare elements.

How to take the value of the model domain

In snippet 4, we discussed the post-conditions of the peek () method. This condition ensures that the priority of the return value of the peek () method is greater than or equal to the priority of all elements in the model domain elementsInQueue. So the question is, how can a model domain like elementsInQueue be valued? Pre-conditions, post-conditions, and invariants all have no side effects, so you cannot use them to set the value of the model field.

JML uses a represents statement to associate the model domain with the specific implementation domain. For example, the following represents statement is used to assign a value to the model field isMinimumHeap:

/ / @ private represents isMinimumHeap

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.