Date of Award

5-2017

Document Type

Thesis

Degree Name

Master of Science (MS)

Legacy Department

Computer Science

Committee Member

Dr. Murali Sitaraman, Committee Chair

Committee Member

Dr. Brian Dean

Committee Member

Dr. Feng Luo

Abstract

This thesis presents a non-trivial candidate software component assembly that presents an opportunity and a challenge to the progress towards automated verification. It presents an opportunity because the data abstraction implementation can serve as a proof of concept of the idea that well-designed and well-annotated software components with mathematical specifications and well-engineered implementation(s) lead to generated verification conditions (VCs) of correctness that are "obvious" to prove. It presents a challenge because verification of the implementation involves multiple theories and the use of a tree concept that is based on a general tree theory for which there are no special-purpose solvers. The thesis contains a specification for a conceptualization of a tree with a position that makes it easy to explore and navigate a tree even as it avoids any explicit references to simplify reasoning. The thesis also contains concept enhancements for trees and an implementation layered using trees for a data abstraction for searching (a version of maps). A key contribution is the development of the implementation so that it is amenable for verification with internal assertions such as representation invariants and abstraction relations, operation specifications, loop invariants, and progress metrics, all of which involve the general tree theory.

Share

COinS