The Java Modeling Language (JML)

Examples of JML Specifications

This page contains links to examples of JML specifications that may be useful to those learning JML or looking for ways of doing things. See also the documentation page for examples that have surrounding explanatory text.

• The Java-JML project by Amirfarhad Nilizadeh on github, which contains several small Java programs with that have been verified by OpenJML against their specifications.
• The BuggyJavaJML project by Amirfarhad Nilizadeh on github, which contains incorrect versions of the programs in the Java-JML project, each of which contains exactly one bug.
• The OpenJML examples page
• Examples in the Common JML Tools Release
  • Samples
  • Package documentation
• JML specifications for the Java Card API (gzipped tar file), from Nijmegen.
• Kind Software's open source webpage, which includes specified versions of the KOA Platform for e-Voting Experimentation, which is "specified and partly verified" using JML. This page also gives access to a newer e-voting system, DiVS, a Danish Voting System implementation, specified using Business Object Notation (BON) and JML and "verified using formal methods".
• A page of examples from the EventB2Java Rodin plug-in. These include a Mass Transport System, a Social Event planner, and several smaller examples such as binary and linear search.

Examples in the Common (formerly ISU) Tools Release

The following are examples of JML specifications contained in the current release of the common (formerly ISU) JML tools.

Samples

The samples directory contains many different samples of JML specifications, including samples used in the other documents. (See also the package documentation for more examples of JML specifications.) The following describes the individual samples in the release.

• The org.jmlspecs.samples.dbc package and its source directory.
• The org.jmlspecs.samples.digraph package and its source directory.
• The org.jmlspecs.samples.dirobserver package and its source directory.
• The org.jmlspecs.samples.jmlkluwer package and its source directory.
• The org.jmlspecs.samples.jmlrefman package and its source directory.
• The org.jmlspecs.samples.jmltutorial package and its source directory.
• The org.jmlspecs.samples.list package and its source directory.
• The org.jmlspecs.samples.list.iterator package and its source directory.
• The org.jmlspecs.samples.list.list1 package and its source directory.
• The org.jmlspecs.samples.list.list2 package and its source directory.
• The org.jmlspecs.samples.list.list3 package and its source directory.
• The org.jmlspecs.samples.list.node package and its source directory.
• The org.jmlspecs.samples.list.node2 package and its source directory.
• The org.jmlspecs.samples.misc package and its source directory.
• The org.jmlspecs.samples.prelimdesign package and its source directory.
• The org.jmlspecs.samples.reader package and its source directory.
• The org.jmlspecs.samples.sets package and its source directory.
• The org.jmlspecs.samples.stacks package and its source directory.
• The org.jmlspecs.samples.table package and its source directory.

Package documentation

The release contains much jmldoc-produced documentation that can also be seen as examples of JML specifications. Aside from the samples above, this includes the following package documentation.

JML-specific packages for users of JML

• The org.jmlspecs.lang package and its source directory.
• The org.jmlspecs.models package and its source directory.
• The org.jmlspecs.models.resolve package and its source directory.
• The org.jmlspecs.jmlunit.strategies package and its source directory.
• The org.jmlspecs.jmlrac.runtime package (whose source directory is not included in the release). This package includes the method JMLChecker.setLevel(int), which can be used to control the assertion checking level at runtime.
• The org.jmlspecs.jmlunit package (whose source directory is not included in the release). This includes the class JMLTestRunner.

Java-specific packages for users of JML

• The java.awt.event package and its source directory.
• The java.io package and its source directory.
• The java.lang package and its source directory.
• The java.lang.reflect package and its source directory.
• The java.math package and its source directory.
• The java.net package and its source directory.
• The java.security package and its source directory.
• The java.sql package and its source directory.
• The java.util package and its source directory.
• The java.util.regex package and its source directory.

Packages from the JML implementation for developers

The following is an entry point for the documentation of the current release of the common (formerly ISU) JML tools. The source code for most of these packages is not included in the release.

• Index of packages in the implementation of the JML common tools.

Last modified Wednesday, July 10, 2024.