A specification language design for the Java Modeling Language (JML) using Java 5 annotations有关JAVA语言设计的国外08年的博士论文-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.