Library JMLSyntax

This file is part of

A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking

Ph.D. Thesis by Hermann Lehner
Online available at

  • Hermann Lehner
  • David Pichardie (Bicolano)
  • Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)

This file can be "Require Import"ed by clients of the full syntax formalisation.

Require Export JMLProgramPlusImpl.
Require Export JMLFull2BasicImpl.
Require Export JMLNotations.

Require Export ZArith.
Require Export List.

Open Scope Z_scope.
Open Scope jml_scope.