Abnormal behavior
The aforementioned behavior specification requests to call the PEEK () and POP () methods, the queue cannot be empty, but it is actually possible to call these two methods when the queue is empty. If this happens, these two methods will throw a NosuchelementException. Exception. We must fix the behavioral norms we have developed in front, allowing this possible possible happening. In this case, we want to use JML's Exceptional_behavior statement.
To current, our behavior is still headed by public Normal_Behavior. Here normal_behavior keywords indicate that this is a normal behavior, and the method will not throw any exceptions. Using the public exceptional_behavior tag can be used to describe the behavior of throwing exceptions. The following code segment shows the exception part of the behavior specification of the PEEK () method in class priorityQueue:
Code section 9 Exceptional_behavior tag
/ * @
@ public normal_behavior
@ Requires! ISempty ();
@ Ensures ElementSinQueue.has (/ Result);
@ a a
@ Public Exceptional_Behavior
@ Requires iesmpty ();
@ Signals (Exception E) E InstanceOf NosuchelementException;
@ * /
/ * @ pure @ * / Object peek () throws nosuchelementException;
Like all examples we saw before, the first part of this specification also starts with public normal_behavior, indicating normal behavior; difference, this specification has a second part, starting with public exceptional_behavior, describing an abnormal behavior. Like the Normal_Behavior statement, the Exceptional_behavior statement also has a Requires statement. This Requires statement indicates that the conditions that must be met when the exceptions listed in the Signals statement are thrown. In the example above, if the ISEMPTY () method returns true, peek () will throw a NosuChelementException exception.
Signals Statement Signals statement is a statement such as Signals (E E) R, where E is an Exception class itself or a subclass, R is an expression. JML explains a signal statement as follows: If there is an exception that is an exception, check whether it is R true. If so, it will perform the established specification; otherwise, throw a unchecked exception (the translator Note: unchecked Exception is called RuntimeException, about these two concepts, please refer to the Java language About exception), to represent our program code Violation of the requirements of the Exceptional_Behavior specification.
The Signals statement in the peek () method is meaningful if the queue is empty, throws a NosuChelementException exception. If the peek () method throws other exceptions that are not NosuChelementexception in the run, then JML will treat this as an error because e instanceof nosuchelementexception is not True. If you want to handle NosuchelementException anomalies, you can modify the Signals statement above, change to Signals (Nosuchelementexcection E) TRUE;. This means that if the peek () method throws a NosuCheLementexception exception, True must be true, and true is a constant, which can always meet the conditions, so that the NosuChelementexception exception can be performed normally. However, we have not mentioned other information about other abnormalities, and the peek () method can throw its signature (translator Note: The signature of the method is the various parts of the method declared, specifically, the method name, parameter Type, return type, and throw an exception, any exception allowed. Its signature says it can throw NOSUCHELEMENTEXCEPTION, which means it can throw both Nosuchelementexception and throw RuntimeException. If there are some elements in the queue and when we call the peek () method, you still throw a NosuChelementException exception (or other exception), JML running assertion check will throw a unchecked Exception, which means that the normal back condition failed.
Conclusion This paper briefly introduces the concept of JML, indicating its contribution to the analysis and design of the surface-to-object system, demonstrating how to use JML tags in the Java program. You can download the complete code used in this article from the resources listed below, and you can find more information about JML.
You can use an open source JML compiler to compile you code with JML tags, and generated class files automatically check the JML specification at runtime. If your program does not implement things specified in the norm, JML will throw a unchecked exception to clear which specification is contrary to it. This can help us capture bugs in the program, and we can ensure that our code is uniform with the document (documentation in JML format).
JML Operation Assessment Inspection The compiler is the first JML tool, and other related tools also have JMLDoc and JMLUnit, and more. JMLDoc is similar to Javadoc tool, and is different. It contains JML specification in the generated HTML format document; JMLUnit can make a framework for a Java class file test, which allows you to easily use Junit tools to test JAVA code containing JML tags . You can also find other related content about JML from the resources listed below.
Here, I will allow me to express my deep gratitude to Gary Leavens and Yoonsik Cheon, who helped me solve some questions about JML and review this article you saw.
Resource
Download the source code used herein.
SourceForge is a JML specification, open source JML tool such as JML compiler, JMLDoc, JMLUnit, and homepage.
The PriorityQueue interface and the BinaryHeap class are part of the open source project Jakarta Universal Collection Components (JCCC).
"JML design start" in Gary T. Leavens, Albert L. Baker and Clyde Ruby (Iowa State University Computer Science, January 2003) is a more detailed introduction to JML. BERTRAND Meyer is a discussion of the design of the object-oriented software, and the second edition of the Decoction (Prentice Hall, 1997).
Granville Miller Introducing object-oriented system modeling about Java modeling section (developerWorks, 2002).
Eric Allen discusses some assertion check restrictions in books in Diagnosing Java Code: Assertions and Temporal Logic in Java Programming (DeveloperWorks, July 2002).
Kyle Brown discusses how to combine analog data objects with hierarchical tests in the article "A Stepped Approach to J2ee Testing With SDAO" (DeveloperWorks, March 2003).
For all aspects of the Java program, please refer to the IBM DeveloperWorks Java area.
Finished>
Please refer to other parts:
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 starts --- Use JML to improve your Java program (2)
http://www.9cbs.net/develop/read_article.asp?id=19200
JML starts --- Use JML to improve your Java program (3)
