You are here

Implementation of Refining Statements in OpenJML and Verification of Higher Order Methods with Model Program Specifications

Download pdf | Full Screen View

Date Issued:
2017
Abstract/Description:
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.
Title: Implementation of Refining Statements in OpenJML and Verification of Higher Order Methods with Model Program Specifications.
17 views
7 downloads
Name(s): Gurramkonda, Sai Chandesh, 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: 2017
Publisher: University of Central Florida
Language(s): English
Abstract/Description: 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.
Identifier: CFE0006743 (IID), ucf:51831 (fedora)
Note(s): 2017-08-01
M.S.
Engineering and Computer Science, Computer Science
Masters
This record was generated from author submitted information.
Subject(s): Higher Order Methods -- OpenJML -- Model Program Specifications -- Refining Statements
Persistent Link to This Record: http://purl.flvc.org/ucf/fd/CFE0006743
Restrictions on Access: public 2017-08-15
Host Institution: UCF

In Collections