The Java Modeling Language (JML) follows the design by contract paradigm. It admits the specification of Java programs, using Hoare style pre- and postconditions and invariants. The specifications are added as comments to the Java program, which hence can be compiled with any Java compiler.