Home

Anonymous Gary T. Leavens

JML Wiki

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules (as in design by contract—DBC). It has many tools to do assertion checking, documentation generation, unit testing, static checking, verification, etc.

Tools

See the JMLSpecs web site for information on downloading various JML tools.

OpenJML

OpenJML is the next generation of the core JML tools and supports Java 1.7. It is based on OpenJDK.

Other Projects and Experimental Efforts

  • [JAJML] is an experimental implementation of JML based on JastAdd. 
  • [JMLTests] is a subproject devoted to creating a common testing framework that incorporates the test corpus from [JML2] and can be used by the developers of a variety of JML-based tools. 
  • [JmlEclipse] offers experimental support for JML via the Eclipse JDT compiler. [JmlEclipse] offers preliminary support for the JML Intermediate Representation ([JIR]), Java Contracts (JC) and more. It has been largely inspired by the following (now superseded) projects:
    • [JML4] is a project that investigated a deep embedding of JML tools in the Eclipse JDT.
    • [JML6] is an incomplete, experimental implementation of JML features using Java annotations and Java Contract (JC).
  • OpenJIR is an experimental version of [OpenJml] supporting the embedding of JML specifications into class files in the form of [JIR].
  • [SafeJML] is a new variant of JML designed to specify Safety Critical Java (SCJ) programs.
  • [temporalJML] is an extension of JML that supports specification and checking of temporal properties of programs.
  • [DevelopmentNotes] on future directions for JML and JML tool support. 

Legacy Tools

The first publicly available JML tool suite, the Common JML Tools or "JML2", targeted Java 1.4 and earlier.

Documentation

Examples

Semantics and Discussion Summaries

Specifications

  • [JML2] Javadoc API
  • [OpenJml] Javadoc API
  • A Beginner's Guide to Specification Writing
  • Specification Writing MobiusPve? workspace

Teaching Materials

JML is used in a variety of courses, from early undergraduate through post-graduate, and in industrial and research tutorials. Several people have also developed screencasts and other online resources on formal methods techniques using JML. We’ve begun collecting these materials and links to other resources on our Teaching Materials page.

Credit



Related

Wiki: DevelopmentNotes
Wiki: JAJML
Wiki: JIR
Wiki: JML2
Wiki: JML4
Wiki: JML6
Wiki: JMLTests
Wiki: JavaContracts
Wiki: JmlDocumentation
Wiki: JmlEclipse
Wiki: OpenJir
Wiki: OpenJml
Wiki: SafeJML
Wiki: SemanticDiscussionIndex
Wiki: TeachingMaterials
Wiki: space.menu
Wiki: temporalJML

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks