Abstract
The Java Modeling Language (JML) describes the functional behavior of Java classes and methods using pre- and postconditions. However, standard pre- and postcondition specifications cannot verify calls to higher order methods (HOMs). JML uses model program specifications to reason about HOMs. This thesis describes the implementation of model programs in the OpenJML tool. The implementation includes parsing, type checking, and matching of model program specifications against the code.
Notes
If this is your thesis or dissertation, and want to learn how to access it or for more information about readership statistics, contact us at STARS@ucf.edu
Graduation Date
2017
Semester
Summer
Advisor
Leavens, Gary
Degree
Master of Science (M.S.)
College
College of Engineering and Computer Science
Department
Computer Science
Degree Program
Computer Science
Format
application/pdf
Identifier
CFE0006743
URL
http://purl.fcla.edu/fcla/etd/CFE0006743
Language
English
Release Date
August 2017
Length of Campus-only Access
None
Access Status
Masters Thesis (Open Access)
STARS Citation
Gurramkonda, Sai Chandesh, "Implementation of Refining Statements in OpenJML and Verification of Higher Order Methods with Model Program Specifications" (2017). Electronic Theses and Dissertations. 5510.
https://stars.library.ucf.edu/etd/5510
Included in
Accessibility Statement
This item was created or digitized prior to April 24, 2027, or is a reproduction of legacy media created before that date. It is preserved in its original, unmodified state specifically for research, reference, or historical recordkeeping. In accordance with the ADA Title II Final Rule, the University Libraries provides accessible versions of archival materials upon request. To request an accommodation for this item, please submit an accessibility request form.