JML2

JML2 is the name of the active codebase for the current (5.5+) release of the JML Common Tools. This page contains links and descriptive notes to help developers working with or reading from JML2.

Features

• Supports Java 1.4.2 completely(?), limited(?) support for Java 5+.
• Runtime assertion checking
• Static checking of most of the features documented by the JML reference manual

Design

The static checker and RAC support is designed in the form of two basic patterns: Interpreter and Visitor.

The Interpreter pattern

The Interpreter pattern is good for modularizing a language's constructs within a language processor. For JML2, the grammar for Java+JML is reflected in a class hierarchy of grammar productions. This hierarchy is rooted at JCompilationUnit, because this is the starting production of the Java+JML grammar. JML2 loosely follows these guidelines in its application of Interpreter:

• each meaningful alternative within a JML-significant nonterminal receives its own subtype in the existing hierarchy
• each object's accessors reveal references to the nonterminals within a particular production

Most of the JML-specific modifications to this grammar exist at the level of declarations, statements and expressions. See the JML reference grammar for more information on the structure of JML's annotations.

The Visitor pattern

Visitor is used to modularize the supported analyses of JML, where possible.

Directory Layout

What exists and where if you checkout JML2 from cvs.