JML is a behavioural interface specification language for Java modules.
JML inherits ideas from Eiffel, Larch and the Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer.
JML specifications are added to Java code in the form of annotations in comments.
Java comments are interpreted as JML annotations when they begin with an @ sign.
These are combined to provide formal specifications of the properties of classes, fields and methods.