Skip to content

rocq-community/jmlcoq

Repository files navigation

JMLCoq

Docker CI Nix CI Contributing Code of Conduct Zulip

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

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.

About

Coq definition of JML and a verified runtime assertion checker [maintainer=@palmskog]

Topics

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Contributors 2

  •  
  •