Java Modeling Language (JML)

Another pitfall caused by this bug is that the jtest script that we have
doesn't work as one might expect. Suppose one has a class C that
implements an interface I. Then executing

jtest C.java
jmlrac C

doesn't test C properly, because the interface I, where some
specifications may be found, is not compiled with jmlc, but instead by
javac, which does get compile I, since it is out of date.

Franco Luque also reported this problem. He wrote in response to Yoonsik
Cheon's clarification:

> It looks like that Provider.java wasn't compiled with jmlc. Try
> jmlc Client.java Provider.java
> and see whether you have the same symptom; you have to list all the
source
> code files as arguments to jmlc.

So that was the problem... I am using NetBeans and my "compile-single"
ant target was correctly compiling with JMLC the selected class, but
was compiling without JMLRAC all its dependencies and overwrinitg the
previously JMLC compiled versions. That was because i was not telling
JMLC where to find the already compiled classes (via the classpath).

Now its fixed, so that it does not overwrite already compiled classes,
but it still compiles without JMLRAC those dependencies that were not
previously compiled. This is on purpose, isn't it? Why?

Logged In: YES
user_id=633675

I would also add the following comment from another user (W.
Craig Trader) on the JML interest list:

One of the biggest problems with JMLC (either with or
without Ant) is the lack of internal dependency checking.
JMLC will always recompile a class, even if none of the
source dependencies for that class have changed. This
results in significant delays when you change one class in a
project that is composed of hundreds of classes.