Design By Contract and JML
Recently, I’ve had the experience of using Java Modeling Language (JML), and its set of tools. This set of tools consists of: ESC/Java2, a static checker that attempts to prove the JML specifications without actually running the program, the Runtime Assertion Checker (RAC), which validates the JML specifications while the program is running, and will throw exceptions if any specification is not satisfied, and JMLUnit, which creates JUnit tests from the JML specifications. In this entry, I will be specifically focusing on JML itself and not any of the additional tools.
The concept of designing each method to adhere to a specific set of preconditions and postconditions was not entirely new to me; however, I had not previously had any experience explicitly specifying these conditions. These conditions had always been a sort of abstract set of thoughts that were laid out while creating a method, and were usually described, to some extent, in the method’s Javadoc. It wasn’t until JML that I actually had to be able to satisfy and prove to JML that the conditions I specified. This meant that JML had to be sure that the conditions that I specified were always going to be satisfied upon entrance, exit, and at every point inside the method where control left the method’s class. This is not as easy as it may sound, and as I had assumed it would be at first.
To be continued…
This entry was posted on Monday, May 4th, 2009 at 3:40 am and is filed under Java. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.
