Amal Jamil Ahmed, Mitchell Wand, Cormac Flanagan
Date of Award
Doctor of Philosophy
Department or Academic Unit
College of Computer and Information Science.
Design, Programming Languages, Semantics, Software Contracts
Computer Sciences | Programming Languages and Compilers
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.
Dimoulas, Christos, "Foundations for behavioral higher-order contracts" (2012). Computer Science Dissertations. Paper 22. http://hdl.handle.net/2047/d20002848
Click button above to open, or right-click to save.