Safe and effective contracts

This dissertation introduces a framework enabling the dynamic verification of expressive specifications. Inspired by formal verification methods, this framework supports assertion, framing, and separation contracts. Assertion contracts specify what code should do, whereas framing contracts specify what code must not do. Separation contracts, inspired by separation logic, combine an explicit assertion contract with an implicit framing contract. In addition to supporting these expressive contracts, this framework also enables assertions to call existing code with side effects while ensuring that successful assertions do not affect the rest of the program. Contracts are guaranteed safe while remaining easy to write. This dissertation introduces a single interface, the delimited checkpoint, that supports all of the contracts listed above. Similar to previous work on equipping a programming language with first class stores, checkpoints represent a state in time. Computations can be run with memory restored to a checkpoint state. Checkpoints augment existing work with a novel family of difference operations that compare two checkpoints, revealing how the intervening computation interacted with memory. Additionally, checkpoints are delimited: they can only be used within a limited scope. This interface suffices to build assertion contracts that support time travel, framing contracts, and separation contracts. Additionally, it supports a novel suppression contract, allowing assertions to safely run existing code by suppressing proscribed effects. A formal operational semantics precisely defines the checkpoint interface, enabling formal reasoning about derived contracts. In particular, the derived contracts provably satisfy key properties. For example, the defining property of separation logic, the frame rule, provably holds for the derived separation contract. Additionally, this dissertation notes the utility of restricting checkpoints to a given (dynamic) scope, giving rise to delimited checkpoints. Contracts do not need the full power of checkpoints, using checkpoints in only a delimited manner. This restriction is useful as it enables delimited checkpoints to reuse the infrastructure needed to support Software Transactional Memory systems. This dissertation presents a prototype implementation of delimited checkpoints based on this observation. Extending the GHC compiler for Haskell, the implementation supports all of the contracts previously discussed.