Quantification (Translator Note: The meaning of the usual term is relatively similar to logic, rather than the quantifier understanding in ordinary sense.)
In the behavioral specifications of the POP () method, we said that its return value is equal to the return value of the peek () method, but we don't see the specifications for the Peek () method. PEEK () method in priorityQueue, please see the following code:
Code Segment 3 PriorityQueue Code Specification for Peek () Method
/ * @
@ public normal_behavior
@ Requires! ISempty ();
@ Ensures ElementSinQueue.has (/ Result);
@ * /
/ * @ pure @ * / Object peek () throws nosuchelementException;
The JML tag requires only when at least one element is included in the queue, the PEEK () method can be called, and the return value of the method must be within ElementSinqueue, that is, this return value must be an element in this queue. .
Note / * @ pure @ * / Indicates that the peek () method is a pure method, and the pure method refers to a method without side effects. JML is only allowed to use a pure method to assert confirmation, so we declare the peek () as a pure method so that we can use the peek () method in the back conditions of the POP () method. Everyone will definitely want to know why JML only allows the use of pure methods to assert confirmation? The problem is this, if JML allows the use of non-pure methods to assert the assertion, we will write a certain behavioral specification for side effects. For example, there will be such a situation, after the assertion confirmation, our code is correct, but if the assertion is banned, our code can not run, or run an error. This is of course not! Later, we will further discuss the problem of side effects.
Inheritance
The JML behavioral specification can be inherited by subclass (including sub-interface) or to implement interfaces, this is different from J2SE1.4 interrupt. JML Keyword ALSO represents the currently defined behavioral specification works with the ancestors or behavioral specifications defined in the interface being implemented. Thus, the behavior specification of the PEEK () method defined in the PriorityQueue interface is equally applicable to the PEEK () method in the BinaryHeap class. This means that although there is no clear definition in binaryheap.peek (), the return value of binaryheap.peek () must also be in ElementSinQueue.
Big top stacks and small tops (translator Note: Big top stacks and small piles are the concepts in the data structure, representing different implementations of the heap sorting method. Sorting is a method of sorting by adjusting the binary tree.) The actions we have defined above have significantly lack of one, that is, we have no maximum priority if we don't require the elements that it returned. Obviously, JCCC's priorityQueue interface can be used for both large top stacks or small piles. The performance of large top stacks and small piles is somewhat different, and the highest-priority of the highest priority in small piles is the smallest, and the highest-priority in the large top stack is the largest. Because PriorityQueue does not know that you are used to make large top stacks or sort, specify which element specification must be defined in the class that implements the PriorityQueue interface.
In JCCC, class BinaryHeap implements the PriorityQueue interface. BinaryHeap allows its customer code to specify a sorting scheme through a parameter in a constructor, which is specified by parameters to sort by large top stacks or by small top stacks. We use a Boolean model variable ISMINIMUMHEAP to determine whether binaryHeap sorting is a large pile or a small pile. The following example is the behavior specification defined by binaryheap to the peek () method: code segment 4 binaryheap class PEEK () method behavior specification
/ * @
@ a a
@ Public normal_behavior
@ Requires! ISempty ();
@ Ensures
@ (Isminimumheap ==>
@ (/ For Object Obj;
@ Elementsinqueue.has (obj);
@ CompareObjects (/ Result, OBJ)
@ <= 0)) &&
@ (! IsminimumHeap ==>
@ (/ For Object Obj;
@ Elementsinqueue.has (obj);
@ CompareObjects (/ Result, OBJ)
@> = 0))));
@ * /
Public Object Peek () THROWS NOSUCHELEMENTEXCEPTION
The rear condition in the above-level code segment 4 contains two parts, which are used for large top stacks and small piles, respectively. The meaning of "==>" symbol is included (the translator Note: This containing the meaning contained in logic). X ==> Y is when it is only when Y is true or x is a true value. For small pile sorting, apply the code listed below:
(/ FORALL OBJECT OBJ;
Elementsinqueue.has (OBJ);
CompareObjects (/ result, obj) <= 0)
The above code / forall is a JML quantifier. The above / forel expression is true when all object OBJ meets ElementSINQUE.has (OBJ). In other words, when comparing using CompareObjects (), the return value of the PEEK () method must be less than or equal to the value of each element in the ElementsInqueue. Other JML quantomes are also / exists, / sum, and / min, and more.
The comparison of the BinaryHeap class is allowed to compare the size of the elements in two ways. One way is to perform comparison elements to implement the Comparable interface, and the comparison process uses the method defined in the element. Another method is that the customer class is incorporated into a Comparator object when constructing a BinaryHeap class, and compares using the Comparator object. Regardless of which comparison method is used, we use the model domain Comparator to represent the comparrator object used in the comparison. In the rear condition of the PEEK () method, the CompareObjects () method uses the comparison mode of the client to perform an element. The compareObjects () method is defined as follows: Code Segment 5 CompareObjects () method
/ * @
@ public normal_behavior
@ Ensures
@ (Comparator == null) ==>
@ (/ Result == (Comparable) a) .compareto (b)) &&
@ (Comparator! = Null) ==>
@ (/ Result == Comparator.com);
@
@ Public Pure Model Int CompareObjects (Object A, Object B)
@ {
@ IF (m_comparetor == null)
@ Return (Comparable) a) .compareto (b);
@ else
@ Return M_comparetor.comPare (a, b);
@}
@ * /
The other keyword model is used in the definition of the CompareObjects method. It means that the CompareObjects method is a model method. Model method is only the JML method in the behavioral specification. The model method is defined in the Java annotation, so the regular Java code cannot be used.
If the customer code of the BinaryHeap class specifies a special Compare to compare, M_Comparator points to the Comparer, otherwise the value of m_comparator is NULL. The CompareObjects () method checks the value of the M_Comparator, and then performs a comparison between the elements.
How to get the value in the model domain we discussed the back conditions of the PEEK () method in the code segment 4. This condition guarantees 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 there is a problem, how is the model domain like ElementSinqueue? The front condition, the rear conditions and invariases are no side effects, so they cannot be used to set the value of the model domain.
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 of the model domain ISMINIMUMHEAP:
@ private represents isminimumHeap <- m_isminheap;
This statement means that the value of the model isminimumHeap is equal to the value of m_isminheap, where m_isminheap is a private Boolean variable in the BinaryHeap class. Once ISMINIMHEAP is required, JML will assure the value of m_isminheap to it.
The REPRESENTS statement does not limit <- The right side must be a member variable. For example, the following is the REPRESENTS statement of ElementSinqueue: code segment 6 ElementsInqueue's Represents statement
/ * @ private represents elementsinqueue
@ <- jmlobjectbag.convertfrom
@ Arrays.aslist (m_ereities)
@ .SUBLIST (1, m_size 1));
@ * /
From here we can see that ElementSinQueue elements are array m_elements [] list from the first element to the M_SIZE element with a list of M_SIZE elements, where array m_efficients [] is a private member of BinaryHeap, used to store priority The elements in the queue, M_SIZE are the number of elements that are being used in M_Elements []. The class binaryheap did not use M_Elements [0], which simplifies the operation of the index. JMLObjectBag.convertFrom () The role is to convert a LIST structure into a JMLObjectBag structure required for ElementsInqueue. This requires the value of ElementSinQueue when the JML is run, and the system calculates the REPRESENTS statement <- the code on the right side of the symbol.
Let's take a look at side effects and abnormal behavior.
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=19200 JML start --- use JML to improve your Java program (3) http://www.9cbs.net/develop/read_article.asp?id=19202 JML start --- use JML improvement Your Java program (4)
