Contracts for first-class modules

9 years 8 months ago
Contracts for first-class modules
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 ...
T. Stephen Strickland, Matthias Felleisen
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where DLS
Authors T. Stephen Strickland, Matthias Felleisen
Comments (0)