Computer Science

Colloquium Details

Behavioral Software Contracts

Abstract

A viable market of software components needs software contracts. These contracts must specify each party's obligations. To ensure that both sides meet their obligations, the market must also agree on standards for monitoring contracts and for assigning blame for contract violations. Unfortunately, in the world of object-oriented components and runtime enforced behavioral contracts, these standards are woefully inadequate. In object-oriented languages (such as Eiffel) contract monitors are deeply flawed. They may assign blame for contract violations to innocent parties or may even ignore contract violations, resulting in incorrect final answers. Even worse, the world of modules and higher-order functions completely lacks behavioral contracts and contracts checkers. My talk explains how object-oriented contract monitors are flawed and how to design a well-founded monitoring system. In addition, it explains how to dynamically check behavioral contracts in languages with higher-order functions. Finally, I present a contract soundness theorem for both worlds. This theorem, which I developed in analogy to Milner's type soundness theorems, is a first step in bringing a theoretical underpinning to contract checking.

Biography

Robert Findler is a Ph.D. candidate in the Department of Computer Science at Rice University. He received his B.S. in Computer Science and Mathematics from Carnegie Mellon University.