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)

Restricted to the UCF community until August 2017; it will then be open access.

Share

COinS