archives

Adapting the Java Modeling Language for Java 5 Annotations


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Taylor, Kristina B., Rieken, Johannes and Leavens, Gary T. (2008) Adapting the Java Modeling Language for Java 5 Annotations. Technical Report 08-06, Computer Science, Iowa State University.

Full text available as:Adobe PDF

Abstract

The Java Modeling Language (JML) is a formal specification language for Java that allows to express intended behavior through assertions. Currently, users must embed these assertions in Java comments, which complicates parsing and hinders tool support, leading to poor usability. This paper describes a set of proposed Java 5 annotations which reflect current JML assertions and provides for better tool support. We consider three alternative designs for such annotations and explain why the chosen design is preferred. This syntax is designed to support both a design-by-contract subset of JML, and to be extensible to the full language. We demonstrate that by building two tools: Modern Jass, which provides almost-native support for design by contract, and a prototype that works with a much larger set of JML.

Keywords:JML, Modern Jass, Java, Specification, Annotation
Subjects:Software: PROGRAMMING TECHNIQUES (E)
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:00000579
Deposited by:Kristina B. Taylor on 09 June 2008



Contact site administrator at: ssg@cs.iastate.edu