The Java Modeling Language (JML) is a formal interface specification language designed for Java. It was developed with the aim of improving the functional software correctness of Java applications. JML has a rich set of features for specifying Java applications, including abstract specifications, method and type specifications, and multiple inheritance specifications. The current JML compiler (jmlc) does not work properly when applied to Java dialects such as Java ME. The instrumented code generated by the original JML compiler uses the Java reflection mechanism and data structures not...