Advisor(s)

Matthias Felleisen

Contributor(s)

Amal Jamil Ahmed, Mitchell Wand, Cormac Flanagan

Date of Award

12-2012

Date Accepted

12-14-2012

Degree Grantor

Northeastern University

Degree Level

Ph.D.

Degree Name

Doctor of Philosophy

Department or Academic Unit

College of Computer and Information Science.

Keywords

Design, Programming Languages, Semantics, Software Contracts

Disciplines

Computer Sciences | Programming Languages and Compilers

Abstract

Contracts are a popular mechanism for enhancing the interface of components. In the world of first-order functions, programmers embrace contracts because they write them in a familiar language and easily understand them as a pair of a pre-condition andsame expressiveness to programmers but their meaning subtly differs from the familiar first-order notion. For instance, it is unclear what the behavior of dependent contracts for higher-order functions or of contracts for mutable data should be. As a consequence, it is difficult to design monitoring systems for such higher-order worlds.

In response to this problem, this dissertation investigates complete monitors, a formal framework for deciding if a contract system is correct. The intuition behind the framework is that a correct contract system should:

1) mediate the exchange of values between contracted components

2) and blame correctly in case of contract violations.

The framework reveals flaws in the semantics for dependent contracts from the literature and suggests a natural fix. In addition, this dissertation demonstrates the usefulness of the framework for language design with a language with contracts for mutable data and a language that mixes typed and untyped imperative programs. The final contribution is the provably correct design of a novel form of contracts, dubbed options contracts, that mix contract checking with random and probabilistic checking.

Document Type

Dissertation

Rights Holder

Christos Dimoulas


View Full Text

Click button above to open, or right-click to save.

Share

COinS