Preliminary Definition of Core JML

The JML specification language has evolved over a number of years and several variations/subsets have been formalized, mainly in the context of prototype sys- tems for runtime and static verification. This document records the preliminary defini- tion of basic semantic concepts for a core fragment of JML. It is intended to facilitate investigation of new features and improvement in interoperability between tools. The formalization is based on a denotational semantics and has been encoded in the PVS theorem prover.