javajml

Is Java Modelling Language executable?

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

Solution

  • 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.