package coq-jmlcoq

  1. Overview
  2. No Docs
Coq definition of the JML specification language and a verified runtime assertion checker for JML

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. H
    Hermann Lehner
  2. D
    David Pichardie
  3. A
    Andreas Kägi

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.12.0.tar.gz
sha512=db60f257f87bba7e41f65f6588aa419b22fd22dd4d377fb07d66f764826ae0690bcb81500f430c921c3bdf471a2eef160c26b50c418c98c1f64220e8c73bf71a

Description

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

Tags

category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:JML keyword:Java Modeling Language keyword:runtime verification logpath:JML date:2020-07-26

Published: 04 Aug 2020

Dependencies (1)

  1. coq >= "8.9" & < "8.13~"

Dev Dependencies

None

Used by

None

Conflicts

None