Is Java Modelling Language executable?

Question

I am studying software engineering course, and there i saw the usage of JML. Here is an example piece of code:

//@ requires f >= 0.0 
public float sqrt(float f) { 
   return f/2;
}

It says that formal JML specifications are executable!

My question is, when we call this sqrt function with f=-4,does this code give an error or throw an exception or give any warnings? I tried it on my computer it just worked well and printed out -2. Then what does it mean that JML are executable? Why don't we use just comments to do this? Can anyone explain?

Thanks

Answer 1

JML is not part of Java. It is an extension designed by a coalition of researchers but without official endorsement. As such, JML annotations are not taken into account by the Java compiler, but you can compile a JML-annotated Java program with a special compiler so that the executable specifications will be taken into account. For instance, JML4C.

Answer 2

Well, this code itself does not create any warning for you. There exist a variety of tools which make use of JML specs, for example:

• jmlrac: test for violations of assertions during execution
• ESC/Java2: static verification; compile-time proving that contracts are never violated
• jmldoc: javadoc-style documentation
• jmlc: assertion-checking compiler
• jmlunit: unit testing tool

In addition to that, JML specs, if properly used, reveal programmer intentions to foreign readers/maintainers of the code.

Answer 3

You are not doing the square root (Math.sqrt(f), see http://docs.oracle.com/javase/6/docs/api/java/lang/Math.html#sqrt(double)) but dividing by 2 (f/2). So there is nothing wrong with that. What you need is using Math.sqrt(...) if this is what I assume you need looking at the name of your method.