Date of Award

8-2018

Degree Type

Thesis

Degree Name

Master of Science in Electrical and Computer Engineering (MSECE)

Department

Electrical and Computer Engineering

Committee Chair

Benjamin Delaware

Committee Member 1

Robert Givan

Committee Member 2

Milind Kulkarni

Abstract

A hallmark of modern programming languages is the strict isolation guarantees they provide to clients and creators of data abstractions, guarantees which are backed by decades-old foundational proofs of representation independence. Recent program synthesis frameworks have exploited these guarantees to ensure that clients are protected from any algorithmic and data structure choices made when producing an implementation from a high-level specification. By their nature, such specifications admit a large number of behaviors, introducing a formal gap between the functional correctness guarantees provided by the synthesis engine and the data abstraction guarantees provided by the programming language. To bridge the gap, this thesis presents System F⊇ , a core calculus for data representation refinement for nondeterministic specifications of abstract data types. This calculus is extensible with user-definable specification predicates. We establish a representation independence theorem for any instantiation of this calculus with compatible user-defined specifications. This theorem justifies replacing a specification with a derived implementation in any client program and is agnostic to the method used to derive an implementation, instead capturing the proof obligations that must be discharged to ensure representation independence.

Download

Share

COinS