coq-jmlcoq.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/coq-community/jmlcoq"
dev-repo: "git+https://github.com/coq-community/jmlcoq.git"
bug-reports: "https://github.com/coq-community/jmlcoq/issues"
license: "MIT"

synopsis: "Coq definition of the JML specification language and a verified runtime assertion checker for JML"
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."""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "dune" {>= "3.5"}
  "coq" {>= "8.10"}
]

tags: [
  "category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms"
  "keyword:JML"
  "keyword:Java Modeling Language"
  "keyword:runtime verification"
  "logpath:JML"
]
authors: [
  "Hermann Lehner"
  "David Pichardie"
  "Andreas Kägi"
]