JML Template Generation

The Java Modeling Language (JML) is a behavioral interface specific language designed to specify Java modules (which are Java classes and interfaces). Specifications are used to describe the intended functionality without considering the way it is implemented. In JML, if a user wants to write specifications for a Java file, he or she must undertake several steps. To help automate the process of creating annotations for method specifications, a tool Jmlspec was created. Jmlspec generated a file that refines the source file and has empty placeholders in which one can write specifications. Although Jmlspec worked with older versions of Java, it does not work with the current version of Java (Java 8). This thesis describes the implementation of a new version of the Jmlspec tool that is compatible with newest versions of Java. This tool will be more maintainable than the older version of Jmlspec and easier to extend