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

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

JML start

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

Use JML to improve your Java program

By Joe Verzulli (Mailto:joe55055@yahoo.com "> joe55055@yahoo.com)

Http://www-106.ibm.com/developerworks/java/library/j-jml.html

The Java Modeling language (Java Modeling Language,JML) is a well-designed symbolic language that encourages you to look at Java classes and methods in a whole new way. In this tutorial, Joe Verzulli, a senior consultant for Java programming, will introduce this new tool and how to use it.

An important principle of object-oriented analysis and design (ooaD) is that procedural thinking should be delayed as much as possible, but most people who follow this principle simply apply it to the level of method implementation. Once the classes and interfaces are designed, the next thing to do is to implement the methods defined in it. Yeah, what else can we do? Is there any other way to use it? After all, programming in Java is the same as programming in other languages, we have to implement each method step by step.

The tag itself simply indicates how to do a thing (how to do something), regardless of what we want to do. It's good if we can know what results we can achieve before we do something, but the Java language does not provide us with a way to explicitly insert this information into our program code.

The Java Modeling language (Java Modeling Language,JML) adds symbols to the Java code that identify what a method is for, but do not care about its implementation. If we use JML, we can describe the expected functionality of a method regardless of how it is implemented. In this way, JML extends this principle of object-oriented design by delaying procedural thinking to method design.

JML introduces a large number of structures to describe behavior, such as model domains, quantifiers, visual range of assertions, preprocessing, post-processing, conditional inheritance, and normal behavior (as opposed to abnormal behavior) specifications. These structures make JML very powerful, but you don't need to understand or use all of the aspects described above, nor do you need to use all of them at once. You can learn a little bit, starting with a very simple one.

This article takes a step-by-step approach to introducing JML. We need to first look at the benefits of using JML, especially the impact on the development and compilation process. Then we will discuss some of the structures of JML, such as pre-conditions, post-conditions, model domains, quantifiers, side effects, abnormal behavior, and so on. At the same time, while discussing these structures, we will give you some routines to give you an intuitive feeling. In this way, through the study of this article, you will have a conceptual understanding of how JML works, and you will be able to apply JML to your own projects.

Overview of JML

Using JML to declaratively describe the expected behavior of a method or class can significantly improve the overall development process. Adding modeling tags to your Java program code has the following benefits:

Can describe more precisely what the code does.

Be able to efficiently find and correct bug in the program

The chance of introducing bug can be reduced when the application is upgraded.

You can find the wrong use of classes by customer code in advance.

Can provide documents in JML format that are completely consistent with the application code

The JML tag is always inside the Java comment, so it has no effect on normally compiled code. If you want to compare the difference between a normal class and a class that uses JML, you can use an open source JML compiler (see sources "> below). If code compiled with the JML compiler does not implement what is required by the JML specification, the runtime throws a JML exception. This feature not only helps us capture bug in our code, but also ensures that documents in JML form are highly consistent with program code.

In the rest of the article, I'll use the PriorityQueue interface and the BinaryHeap class in the open source Jakarta Commons Collection Component (JCCC) project to demonstrate the various properties of JML. Here you can find these two files complete with the JML tag.

Requirements and responsibilities

The code used in this article (see the address below) includes the PriorityQueue interface in the open source project JCCC. Interface, of course, declares the signature of some methods, including the parameter type of the method and the type of the return value, and does not involve the implementation of the method. In general or just as required by the Java syntax, the class that implements the interface simply implements the methods defined in the interface, no matter how bizarre the implementation is. We don't want to do this, we want to be able to determine a behavior specification, and all classes that implement this interface implement the methods defined in this interface in the way we specify. We can do this by using JML.

Consider the pop () method of the PriorityQueue interface. What functional requirements should the pop () method have for priority queues? There should be at least three: first, if the pop () method is to be called, there must be at least one element in the queue; second, the method should return the element with the highest priority in the queue; and third, the method should remove the returned element from the queue.

The following code snippet shows the JML tag indicating that the first requirement is met:

Code snippet 1 JML markup for the functional specification of the pop () method

/ * @

@ public normal_behavior

@ requires! IsEmpty ()

@ * /

Object pop () throws NoSuchElementException

As mentioned earlier, the JML tag is written in comments in the Java code. Multiline comments that contain JML tags begin with / * @, and JML ignores any blank lines that begin with @. If it is a single line, you can also use the / / @ tag.

Here the public keyword in the JML comment has the same meaning as the public in Java, which means that all other classes in the program follow this JML requirement. Public requirements can only be applied to public methods and public member variables. JML also has scope at the private-, protected-, and package- levels. Again, the rules for these scopes are very similar to those in the Java language.

The normal_behavior keyword here means that the JML requirement indicates that this is a normal situation and that the runtime does not throw an exception. Later, we will describe how abnormal behavior is defined.

Precondition and postcondition

The JML keyword requires is used to denote preconditions, which represent requirements that must be met before a method is called. The above code snippet contains a precondition that requires that the call to the pop () method requires that the isEmpty () method return false, which means that the queue contains at least one element.

The postcondition specification of a method indicates the responsibility of a method, that is, when the method returns, it must meet the requirements of the postcondition. In our example above, the pop () method should return the highest priority element in the queue. We want to specify a postcondition that requires JML to check at run time to see if this fact is met. To do this, we must track all the elements added to the priority queue so that we can determine which element the pop () method should return. How do I do that? You might consider adding a member variable to the PriorityQueue interface to store the value of the elements in the queue, but there are two problems with doing so:

PriorityQueue is an interface, it may have a variety of specific implementations, such as binary heap, Fibonacci heap, calendar queue, etc., it should be consistent with its various implementations, and the JML tag should not involve any specific implementation details.

As an interface, PriorityQueue can only have static member variables.

To deal with this situation, JML introduces a concept called model fields.

Model domain

The model domain is similar to member variables and can only be applied to behavioral specifications. This is an example of declaring a model domain in PriorityQueue:

/ / @ public model instance JMLObjectBag elementsInQueue

What this declaration means is that there is a model field called elementsInQueue whose type is JMLObjectBag (this data type is defined in JML). The instance keyword indicates that although the domain is defined in the interface, any class that implements the interface has a separate, non-static elementsInQueue domain. Like other JML tags, this declaration appears in comments, so regular Java code cannot use this elementsInQueue variable. When the program is running, no object has a member variable called elementsInQueue.

Behavior norm and realization

Using a packet to store the elements in the queue, and then checking each element to find out which one has the highest priority can feel inefficient. However, this is only part of the code of conduct and does not involve implementation. The role of the behavior specification is to describe the behavior interface of the PriorityQueue, that is, to specify the external behavior that the client code that uses PriorityQueue can rely on.

Specific implementations of the PriorityQueue interface can use any more efficient approach as long as they meet the requirements of this behavior specification. For example, JCCC has a BinaryHeap class that implements this interface by using a binary heap stored in an array.

However, while there is no need to consider execution efficiency when defining a behavior specification in JML, it is important to check JML assertions at run time. So there may be performance pressure on the program to run when assertion checking is turned on.

ElementsInQueue stores the value of the element added to the priority queue, and the following code snippet shows how the pop () method uses elementsInQueue:

Code snippet 2 uses the model domain in the post-condition of pop ()

/ * @

@ public normal_behavior

@ requires! IsEmpty ()

@ ensures

@ elementsInQueue.equals ((JMLObjectBag)

@ old (elementsInQueue))

@ .remove (esult) & &

Esult.equals (old (peek ()

@ * /

Object pop () throws NoSuchElementException

The ensures keyword indicates that it is followed by a postcondition that must be met when the pop () method returns. Esult is a JML keyword that equals the return value of the pop () method. Old () is a JML function that returns the value of the parameter before the pop () method is called.

This ensures statement contains two postconditions. First, the element returned by the pop () method must be removed from the elementsInQueue. Second, the return value should be consistent with the value returned by the peek () method.

Class-level invariants

We have now seen that JML allows us to specify pre-and post-conditions for methods, and it also allows us to specify class-level invariants. Class-level invariants refer to the conditions that must be met for each method to enter and exit a class. For example, / / @ public instance invariant elementsInQueue! = null; is an invariant of PriorityQueue, meaning that once any class that implements PriorityQueue is instantiated, the value of elementsInQueue cannot be null.

The above is all the content of the article "how to use JML to improve your Java program". 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.