## The Interdependence of Effects and Uniqueness

by John Boyland.

### Abstract

A good object-oriented effects system
gives the ability to define abstract regions (or ``data groups'')
of state within objects that can be extended
in subclasses. Then one can specify (for instance) read and write effects
on these abstract regions.
Additionally, effects on ``wholly owned subsidiary''
objects should be seen as effects on regions of the owning object.
For instance, an assignment within a bucket of a hash table should be
seen as an effect on the hash table alone. Correctness of this
transfer of effects depends on the bucket being accessible only
through the hash table; it must be *unique*.

Uniqueness can be guaranteed using *destructive
reads* (in which a unique variable can be used at most once).
Destructive reads are inconvenient,
so most uniqueness systems permit *borrowing reads*
as well,
in which a temporary alias of a unique variable is permitted. But if
the unique variable is read during the lifetime of this alias, the
uniqueness invariant fails. So we wish to ensure that this read effect
does not happen. For modularity reasons, we use
effects annotations on methods
to check for such read effects.

Thus we see that effects and uniqueness depend on each
other. Our position is that the use of annotations breaks the
cyclic dependence as long as the annotations are given semantics
independent of the analyses. As a semantics of uniqueness annotations
is already available, we then sketch a semantics of effects
annotations independent of uniqueness. Thus decoupled, one can prove
the correctness of a uniqueness analysis and an effects analysis
without regard for the other.

### BibTeX Style Reference

@inproceedings(boyland:01interdependence,
author = {John Boyland},
title = {The Interdependence of Effects and Uniqueness}
booktitle = {3rd workshop on Formal Techniques for Java Programs},
year = 2001,
note = {URL: http://www.informatik.fernuni-hagen.de/import/pi5/workshops/ecoop2001\_papers.html}
nothing = {})

### How to Get a Copy

The workshop papers are available from the workshop
web site. A Postscript preprint
(or PDF) is also available here.

Last Modified: April 10, 2003

The Interdependence of Effects and Uniqueness /
boyland@cs.uwm.edu