Aaron Greenhouse
An Object-Oriented Effects System
An effects systems describes how state may be accessed during the execution
of some program component. This information is used to assist reasoning
about a program, such as determining whether data dependencies may exist
between two computations. We define an effects system for Java that
preserves the abstraction facilities that make object-oriented programming
languages attractive. Specifically, a subclass may extend abstract regions
of mutable state inherited from the superclass. The effects system also
permits an object's state to contain the state of wholly-owned subsidiary
objects. In this presentation, we describe a set of annotations for
declaring permitted effects in method headers, and show how the actual
effects in a method body can be checked against the permitted effects.
April 28, 1999
3:30pm
Wean 8220