Technical Report No. 264 - Abstract

Phillip Heidegger, Annette Bieniusa, Peter Thiemann :
Access permission contracts for scripting languages

The ideal software contract fully specifies the behavior of an operation. Often, in particular in the context of scripting languages, a full specification may be cumbersome to state and may not even be desired. In such cases, a partial specification, which describes selected aspects of the behavior, may be used to raise the confidence in an implementation of the operation to a reasonable level. We propose a novel kind of contract for object-based languages that specifies the side effects of an operation with access permissions. An access permission contract uses sets of access paths to express read and write permissions for the properties of the objects accessible from the operation. We specify a monitoring semantics for access permission contracts and implement this semantics in a contract system for JavaScript. We prove soundness and stability of violation under increasing aliasing for our semantics. Applications of access permission contracts include security, enforcing modularity, test-driven development, program understanding, and regression testing. With respect to testing and understanding, we find that adding access permissions to contracts increases the effectiveness of error detection through contract monitoring by 6-13%.