 | This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. (April 2024) |
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.