You are here

Design of a JMLdoclet for JMLdoc in OpenJML

Download pdf | Full Screen View

Date Issued:
2016
Abstract/Description:
The Java Modeling Language (JML) is a behavioral interface specification language designed for specifying Java classes and interfaces. OpenJML is a tool for processing JML specifications of Java programs. To facilitate viewing of these specifications in a user-friendly manner, a tool JMLdoc was created. The JMLdoc tool adds JML specifications to the usual Javadoc documentation. JMLdoc is an enhancement of Javadoc that adds to the Javadoc documentation the JML specifications that are present in the source code. The JMLdoc tool is a drop-in replacement for Javadoc, with additional functionality and additional options. The current design of JMLdoc uses the standard Javadoc's doclet. The current design lacks the provision for doclet extensions, unlike Javadoc. This thesis proposes a new design which is more aligned with the design of Javadoc and its provision for doclet extensions by implementing a JMLdoclet: a new doclet for OpenJML with support for JML elements. The new design makes JMLdoc independent of Javadoc's internals. This way maintenance is reduced as Javadoc evolves. The new design also combines specifications from inheritance and refinements and presents the complete JML specification to the user. This new doclet based design will be more maintainable and easier to extend.
Title: Design of a JMLdoclet for JMLdoc in OpenJML.
13 views
7 downloads
Name(s): Donthala, Arjun Mitra Reddy, Author
Leavens, Gary, Committee Chair
Turgut, Damla, Committee Member
Jha, Sumit Kumar, Committee Member
University of Central Florida, Degree Grantor
Type of Resource: text
Date Issued: 2016
Publisher: University of Central Florida
Language(s): English
Abstract/Description: The Java Modeling Language (JML) is a behavioral interface specification language designed for specifying Java classes and interfaces. OpenJML is a tool for processing JML specifications of Java programs. To facilitate viewing of these specifications in a user-friendly manner, a tool JMLdoc was created. The JMLdoc tool adds JML specifications to the usual Javadoc documentation. JMLdoc is an enhancement of Javadoc that adds to the Javadoc documentation the JML specifications that are present in the source code. The JMLdoc tool is a drop-in replacement for Javadoc, with additional functionality and additional options. The current design of JMLdoc uses the standard Javadoc's doclet. The current design lacks the provision for doclet extensions, unlike Javadoc. This thesis proposes a new design which is more aligned with the design of Javadoc and its provision for doclet extensions by implementing a JMLdoclet: a new doclet for OpenJML with support for JML elements. The new design makes JMLdoc independent of Javadoc's internals. This way maintenance is reduced as Javadoc evolves. The new design also combines specifications from inheritance and refinements and presents the complete JML specification to the user. This new doclet based design will be more maintainable and easier to extend.
Identifier: CFE0006295 (IID), ucf:51596 (fedora)
Note(s): 2016-08-01
M.S.
Engineering and Computer Science, Computer Science
Masters
This record was generated from author submitted information.
Subject(s): JML -- Design by Contracts -- Doclets -- JMLdoc
Persistent Link to This Record: http://purl.flvc.org/ucf/fd/CFE0006295
Restrictions on Access: public 2016-08-15
Host Institution: UCF

In Collections