The Java Modeling Language (JML) is a specification language for Java programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as Java annotation comments to the source files, which hence can be compiled with any Java compiler. Various verification tools, such as a runtime assertion checker and the Extended Static Checker (ESC/Java) aid development. Overview JML is a behavioural interface specification language for Java modules. JML provides semantics to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. 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. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler. Syntax 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. That is, comments of the form //@ <JML specification> or /*@ <JML specification> @*/ Basic JML syntax provides the following keywords requires Defines a precondition on the method that follows. ensures Defines a postcondition on the method that follows. signals Defines a postcondition for when a given Exception is thrown by the method that follows. signals_only Defines what exceptions may be thrown when the given precondition holds. assignable Defines which fields are allowed to be assigned to by the method that follows. pure Declares a method to be side effect free (like assignable \nothing but can also throw exceptions). Furthermore, a pure method is supposed to always either terminate normally or throw an exception. invariant Defines an invariant property of the class. loop_invariant Defines a loop invariant for a loop. also Combines specification cases and can also declare that a method is inheriting specifications from its supertypes. assert Defines a JML assertion. spec_public Declares a protected or private variable public for specification purposes. Basic JML also provides the following expressions \result An identifier for the return value of the method that follows. \old(<expression>) A modifier to refer to the value of the <expression> at the time of entry into a method. (\forall <decl>; <range-exp>; <body-exp>) The universal quantifier.