Java modeling language

on







JML use to write specifications for a java program. We can say that it is some kind of specification language. Specifications are written as Java annotation comments.

But wait, how does compiler compile the Java comments?? For that, you have to download “openJML” and import it into a compiler. And JML provides some specific keywords that you have to write according to JML format.

There is a code Example for JML:

public class MaybeAdd {
     //@ requires a > 0;
     //@ requires b > 0;
     //@ ensures \result == a+b;
     public static int add(int a, int b){
         return a-b;
     }

    public static void main(String args[]){
         System.out.println(add(2,3));
     }
 }

And here is JML specification:

//@ requires a > 0;
     //@ requires b > 0;
     //@ ensures \result == a+b;

You can run or check that code on openJML. For now, let me explain that code. I know you are good Java programmer. You can see, according to specification result should be the addition of two numbers. But in the code, you can also see return value is (a-b) so the given program is not according to specification. If we go deep inside Java concepts it is not a syntax error and not any compiler is going to catch it for us. It’s a logical error.

 So, here the game begins. As we wrote that specifications so when we run that program JML will warn us something not according to written specification.

Not something. It will give what actually the error is.

“requires” and “ensures” are JML keywords and many more. All are easy to understand. You can check all of them with a complete description. here

Are we mad? we are writing the code and specification with it.

No, we are not. We have to write the specification before writing the code. So, we can say that specification ensures that we are writing right code.

Now, let's change the whole game. What if you don’t have to write code at all?

Yes, it will possible you only have to write specifications than with one click, the compiler will generate code for you. I know, you love to code but save money, save time.

JML specification is written after designing phase. Big companies require that specifications to save they're as** from huge blunders. Specifications and mathematical proves are also required to build formal software. If you don’t know about models and different phases then you can check it. here


If there is any ambiguity you can contact me through email or comments. I will feel good to help you. J  

Beyond Programming


Cheers!


Saifullah




Comments

Post a Comment