JMLCoq

A Coq formalization of the syntax and semantics of the Java-targeted JML specification language, along with a verified runtime assertion checker for JML.

Meta

• Author(s):
  • Hermann Lehner (initial)
  • David Pichardie (initial)
  • Andreas Kägi (initial)
• Coq-community maintainer(s):
  • Karl Palmskog (@palmskog)
• License: MIT License
• Compatible Coq versions: 8.10 or later
• Additional dependencies: none
• Coq namespace: JML
• Related publication(s):
  • A formal definition of JML in Coq and its application to runtime assertion checking doi:10.3929/ethz-a-006680049
  • A Formalization of JML in the Coq Proof System doi:10.3929/ethz-a-006903145

Building and installation instructions

The easiest way to install the latest released version of JMLCoq is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-jmlcoq

To instead build and install manually, do:

git clone https://github.com/coq-community/jmlcoq.git
cd jmlcoq
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

More information about the formalization can be found on the project website.