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.15.0.tar.gz
sha512=2e9d26e4b5517787a03518372902405b5eafda6ff81a1c4a5c51ebbd268d84817183ab12177f18235ee68d930002f5715642b783108ac5f55787cbec83d108be

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:2022-06-26

Published: 10 Sep 2022

Dependencies (1)

  1. coq >= "8.10" & < "8.20"

Dev Dependencies

None

Used by

None

Conflicts

None