Introduction - If you have any usage issues, please Google them yourself
The Java
Modeling Language (JML) is one such specification language for Java that uses comments to specify
contracts. However, starting with version 5, Java has introduced annotations, a syntactical structure
to place metadata in various places in the code. This thesis proposes an initial design to writing JML
contracts in the Java 5 annotation syntax and evaluates several criteria in the areas of specification
languages and Java language design: whether these annotations are expressive enough to take advantage
of annotation simplicity and tool support, and whether the annotation syntax is expressive enough to
support handling a large specification language such as JML.
AspecificationlanguagedesignfortheJavaModelingLanguageusingJava5annotations.pdf