ACL --- Eliminating Parameter Aliasing with Dynamic Dispatch
				  by
		  Gary T. Leavens and Olga Antropova

			       Abstract

We have designed and prototyped a new approach for eliminating reference
parameter aliases. This approach allows procedure calls with overlapping
call-by-reference parameters, but guarantees that procedure
bodies are alias-free. It involves writing multiple bodies for a
procedure: up to one body for each possible aliasing combination.
Procedure calls are dispatched
to the appropriate procedure body based on the alias combination
that occurs among the actual parameters and imported global variables;
errors are generated if there is no corresponding body.
This approach makes writing verifiable client code simpler,
since  clients do not need to write code to determine the aliasing combination
among actuals.
Furthermore, since procedure bodies are free of aliases,
their static analysis and verification is easier.

The prototype language we have designed to explore these ideas
incorporates some features to limit the number of alternative procedure bodies
that a programmer must write.


Keywords:  reference parameter aliasing, global variable aliasing,
multibody procedures, dynamic dispatch, static dispatch, program verification,
ACL language, static analysis, call-by-reference.


1997 CR Categories:
D.3.1 [Programming Languages] Formal Definitions and Theory --- semantics;
D.3.3 [Programming Languages] Language Constructs and Features
      --- control structures, procedures, functions, and subroutines;
D.3.m [Programming Languages] Miscellaneous
      --- dynamic dispatch, multiple dispatch;
F.3.1 [Logics and Meanings of Programs]
      Specifying and Verifying and Reasoning about Programs
      --- logics of programs.