package coq-jmlcoq
Coq definition of the JML specification language and a verified runtime assertion checker for JML
Install
Dune Dependency
Authors
Maintainers
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-26Published: 10 Sep 2022
On This Page