You are here

JML Template Generation

Download pdf | Full Screen View

Date Issued:
2017
Abstract/Description:
The Java Modeling Language (JML) is a behavioral interface specific language designed to specify Java modules (which are Java classes and interfaces). Specifications are used to describe the intended functionality without considering the way it is implemented. In JML, if a user wants to write specifications for a Java file, he or she must undertake several steps. To help automate the process of creating annotations for method specifications, a tool Jmlspec was created. Jmlspec generated a file that refines the source file and has empty placeholders in which one can write specifications. Although Jmlspec worked with older versions of Java, it does not work with the current version of Java (Java 8). This thesis describes the implementation of a new version of the Jmlspec tool that is compatible with newest versions of Java. This tool will be more maintainable than the older version of Jmlspec and easier to extend.
Title: JML Template Generation.
31 views
19 downloads
Name(s): Poojari, Kushal Raghav, Author
Leavens, Gary, Committee Chair
Turgut, Damla, Committee Member
Dechev, Damian, Committee Member
University of Central Florida, Degree Grantor
Type of Resource: text
Date Issued: 2017
Publisher: University of Central Florida
Language(s): English
Abstract/Description: The Java Modeling Language (JML) is a behavioral interface specific language designed to specify Java modules (which are Java classes and interfaces). Specifications are used to describe the intended functionality without considering the way it is implemented. In JML, if a user wants to write specifications for a Java file, he or she must undertake several steps. To help automate the process of creating annotations for method specifications, a tool Jmlspec was created. Jmlspec generated a file that refines the source file and has empty placeholders in which one can write specifications. Although Jmlspec worked with older versions of Java, it does not work with the current version of Java (Java 8). This thesis describes the implementation of a new version of the Jmlspec tool that is compatible with newest versions of Java. This tool will be more maintainable than the older version of Jmlspec and easier to extend.
Identifier: CFE0006641 (IID), ucf:51228 (fedora)
Note(s): 2017-05-01
M.S.
Engineering and Computer Science, Computer Science
Masters
This record was generated from author submitted information.
Subject(s): JML -- JML Template Generation
Persistent Link to This Record: http://purl.flvc.org/ucf/fd/CFE0006641
Restrictions on Access: public 2017-05-15
Host Institution: UCF

In Collections