You are here
JML Template Generation
- 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. |
![]() ![]() |
---|---|---|
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 |