The Geneva convention on the treatment of object aliasing

ABSTRACT

Aliasing has been a problem in both formal verification and practical programming for a number of years. To the formalist, it can be annoyingly difficult to prove the simple Hoare formula {x = true} y := false {x = true}. If x and y refer to the same boolean variable, i.e., x and y are aliased, then the formula will not be valid, and proving that aliasing cannot occur is not always straightforward. To the practicing programmer, aliases can result in mysterious bugs as variables change their values seemingly on their own. A classic example is the matrix multiply routine mult(left, right, result) which puts the product of its first two parameters into the third. This works perfectly well until the day some unsuspecting programmer writes the very reasonable statement mult(a, b, a). If the implementor of the routine did not consider the possibility that an argument may be aliased with the result, disaster is inevitable.

REFERENCES

• 1: [AdB90] Pierre America and Frank de Boer. A sound and complete proof system for SPOOL. Technical Report 505, Philips Research Laboratories, May 1990.
• 2: Craig Chambers , David Ungar, Making pure object-oriented languages practical, Conference proceedings on Object-oriented programming systems, languages, and applications, p.1-15, October 06-11, 1991, Phoenix, Arizona, United States
• 3: [Coo78] Stephen A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, 7(1):70-90, February 1978.
• 4: [HMRC88] Richard C. Holt, Philip A. Matthews, J. Alan Rosselet, and James R. Cordy. The Turing Language: Design and Definition. Prentice-Hall, 1988.
• 5: John Hogg, Islands: aliasing protection in object-oriented languages, Conference proceedings on Object-oriented programming systems, languages, and applications, p.271-285, October 06-11, 1991, Phoenix, Arizona, United States
• 6: Douglas E. Harms , Bruce W. Weide, Copying and Swapping: Influences on the Design of Reusable Software Components, IEEE Transactions on Software Engineering, v.17 n.5, p.424-435, May 1991 [doi>10.1109/32.90445]
• 7: William Landi , Barbara G. Ryder, Pointer-induced aliasing: a problem taxonomy, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-103, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99599]
• 8: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 9: Bertrand Meyer, Object-Oriented Software Construction, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 10: Alan Snyder, Modeling the C++ Object Model, An Application of an Abstract Object Model, Proceedings of the European Conference on Object-Oriented Programming, p.1-20, July 15-19, 1991
• 11: Peter Wegner, Dimensions of object-based language design, Conference proceedings on Object-oriented programming systems, languages and applications, p.168-182, October 04-08, 1987, Orlando, Florida, United States
• 12: Alan Wills, Capsules and Types in Fresco: Program Verification in Smalltalk, Proceedings of the European Conference on Object-Oriented Programming, p.59-76, July 15-19, 1991

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

General Terms:
Design, Languages