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.13.0.tar.gz
sha512=3d2742d4c8e7f643a35f636aa14292c43b7a91e3d18bcf998c62ee6ee42e9969b59ae803c513d114224725099cb369e62cef8575c3efb0cf26886d8bb8638cca

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:2021-08-01

Published: 01 Aug 2021

Dependencies (1)

  1. coq >= "8.10" & < "8.15~"

Dev Dependencies

None

Used by

None

Conflicts

None