Access Permission Contracts for Scripting Languages

Professor Peter Thiemann
University of Freiburg, Germany

Abstract

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%.