Technical Report Number
Software, Computing Methodologies
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.