Jump to content

Java Modeling Language

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Tillmo (talk | contribs) at 21:48, 12 September 2005 (start). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

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.

There are various verification tools for JML, such as a runtime checker and the Extended Static Checker (ESC/Java).

Literature

  • Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. Draft tutorial.
  • Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Kluwer, 1999.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Java_Modeling_Language&oldid=23123384"