archives

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


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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

Abstract

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)
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: ssg@cs.iastate.edu