This is a study on the Java Modeling language, presenting its main features and applying them onto an algorithm based upon Binary Decision Diagrams. JML is a Design by Contract tool for java. The principal idea behind Design by Contract is that clients calling methods in a class have a contract with each other. These contracts consist of pre- and post-conditions that are to be validated before and after the execution of any method with such a contract.
As interesting as it was studying JML, at the implementation stage it became clear that the JML2 tool set was not upgraded for any java upgrades beyond java 1.4. Using generic types and other language features such as the for-each loop was not recognized by the JML compiler.
However, once up and running with a J2SE4 environment, many advantages could be discovered. The runtime assertion checker worked great as a bug prevention tool and the JML specifications serve as a good way to document code properly. More important though is the way it forces the developer to take into consideration all the different relationships between classes and their methods and also to define set invariants to hold for these.