I am a Teaching Assistant preparing an assignment for my students, in order for them to learn anout JML and design by contract. I give 3 files to them : RArray.refines-java (a specification with blank JML assertions), RArray.java (the class which implements the previous spec) and TestRArray.java (a test class).
In order to perform the work, they will have to compute 3 commands :
jmlc RArray.refines-java
(compilation of the specification and the implementation)javac TestRArray.java
(compilation of the test class)jmlrac TestRArray
(verification with jml runtime assertion checker)
In order to do that, however, they have to install JML on the computers at school, where obviously nobody has root access. I tried to install it first, and it appears it does not require any root access - I followed this French tutorial, with this zip file.
I tried on my ubuntu 14.04 laptop, it worked just fine and I have been able to manage some results for the assignment. Even at school, on Fedora, I can install the tools without any complain, and add them to PATH. But, at school, I encounter an error when I run
jmlc RArray.refines-java
.
Here is my error :
$ jmlc RArray.refines-java
parsing RArray.refines-java
parsing RArray1/RArray.java
typechecking RArray1/RArray.java
The .class file 'java/lang/CharSequence.class' appears to be malformed: Bad constant tag: 18
Fatal error - Unable to find a class for java/lang/CharSequence: error: Cannot find type "java.lang.CharSequence"
I tried to search before, and it appears it can be a matter of duplicate CLASSPATHs, or something in those lines, but I could not access it.
I tried also to download the ZIP file again, to verify if this malformed class would be fixed, but no luck.
I tried to run javac RArray.refines-java
, and it compiles as it is supposed to do, thus it must be a jml issue.
Here is the result of java -version
:
java version "1.8.0_66"
Java(TM) SE Runtime Environment (build 1.8.0_66-b17)
Java HotSpot(TM) 64-Bit Server VM (build 25.66-b17, mixed mode)
Here is the result of jml -version
:
Version: Common JML tools release 5.6_rc4 (Mar. 16, 2009)
Do you have any idea on how to fix this? I hope I won't have to discard everything.