[PRL] Torture chamber: Stevie, 10/21, 11:45, WVH366

[Aaron Turon]

Stevie will be giving a practice talk during the PL-Seminar slot this week:

Stevie Strickland
Wednesday, October 21, 2009
11:45-1:30 (Practice talk is for a 30-minute slot)
WVH366

Title: Contracts for First-Class Modules

Joint work with Matthias Felleisen

Abstract:

Behavioral software contracts express properties concerning the flow
of values across component (modules, classes, etc) interfaces. These
properties are often beyond the reach of theorem provers and are
therefore monitored at run-time. When the monitor discovers a contract
violation, it raises an exception that simultaneously pinpoints the
contract violator and explains the nature of the violation.

Currently contract monitoring assumes static module interfaces.
Specifically, the contract compiler partitions a contract into
disjoint obligations for the static modules that communicate to an
interface. At run-time, the information is used for catching and
explaining contract violations. While static modules suffice for many
situations, first-class modules---such as the units provided by PLT
Scheme---support the dynamic and multiple linking that is often
required in open software systems. The problem is, of course, that in
such a world, it becomes impossible to tell from the source program
alone which components have agreed to which contracts.

In this paper, we develop the semantic framework of monitoring
contracts for dynamic modules. We establish the internal consistency
of the semantics, and we sketch an implementation based on our
experience of equipping PLT Scheme with such contracts.