A Specification Language Design for the Java Modeling Language (JML) Using Java 5 Annotations







Deposit Papers 


Taylor, Kristina B. (2008) A Specification Language Design for the Java Modeling Language (JML) Using Java 5 Annotations. Masters thesis, Computer Science, Iowa State University.

Full text available as:Adobe PDF


Design by contract specification languages help programmers write their intentions for a piece of code in a formal mathematical language. Most programming languages do not have built-in syntax for such specifications, so many design by contract languages place specifications in comments. 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.

Keywords:JML annotation specification
Subjects:Software: PROGRAMMING TECHNIQUES (E): General
Software: SOFTWARE ENGINEERING (K.6.3): General (K.5.1)
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Coding Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
ID code:00000568
Deposited by:Kristina B. Taylor on 14 April 2008

Contact site administrator at: