A theory, graphical notation, mathematical calculus and implementation for finding whether two given expressions can, at execution time, denote references attached to the same object. Intended as the seed for a comprehensive solution to the "frame problem" and as an alternative (for the specific issue of determining aliases) to separation logic, shape analysis, ownership types and dynamic frames 1 . You have, most certainly, read Homer. I have not (too much blood), but then I listen to Offenbach a lot, so we share some knowledge: we both understand that "the beautiful daughter of Leda and the swan", "poor Menelaus's spouse" and "Pâris's lover" all denote the same person, also known as Helen of Troy. The many modes of calling Helen are a case of aliasing, the human ability to denote a single object by more than one name. Aliasing is at its highest risk of causing confusion when it is dynamic, that is to say when an object can at any moment acquire a new name, especially if that name previously denoted another object. The statement "I found Pâris's lover poorly dressed " does not necessarily cast aspersion on Helen's sartorial tastes, as Pâris might by now have found himself a new lover; but if we do not carefully follow the lives of the rich and famous we might believe it does. Stories of dire consequences of dynamic aliasing abound in life, literature and drama. There is even an opera, Smetana's The Bride Sold 2 , whose plot entirely rests on a single aliasing event. To the villagers' dismay, Jeník promises the marriage broker, in return for good money, not to dissuade his sweetheart Mařenka from marrying the son of the farmer Mícha. Indeed Mícha wants Mařenka for his dimwit son, Vašek, but it is suddenly revealed that Jeník, believed until then to be a stranger to the village, is Mícha's son from a first marriage: he has tricked everyone. To a programmer, this tale sounds familiar: the equivalent in program execution is to perform an operation on certain operands, and inadvertently to modify a property of a target that is not named in the operation -hence the risk of confusion -but aliased to one of the operands. For example an operation may, officially, modify the value of x.a; but if x denotes a reference and y another reference which happens at the time of execution to be aliased to x (meaning that they both point to the same object), the operation will have an effect on y.a even though its text does not cite y. If b is aliased to a, we might even have an operation that modifies y.b even though its description in the programming language mentions neither y nor b. ___________  It is not hard to justify the continued search for effective verification techniques covering aliasing. In the current state of proof technology, the aliasing problem (together with the closely related frame problem, to which it provides the key) is the principal obstacle preventing full proofs of correctness for sequential programs. It also plays a role in the specific difficulties of proving concurrent programs correct. (For references on the issues and approaches cited in this section, see appendix F.) A symptom of this situation is that industrial program proving tools often preclude the use of pointers altogether. An example is the Spark environment, which has made a remarkable contribution towards showing that production programs can be routinely subjected to proof requirements. Spark relies on a programming language, presented as a subset of Ada but in reality a subset of a Pascal-like language (plus modules), without support for pointers or references. In considering how to make such pioneering advances relevant to a larger part of the industry, it is hard to imagine masses of programmers renouncing pointers and other programming languages advances of the past three decades. The absence of a generally accepted solution is not due to lack of trying. The aliasing problem has been extensively researched, and interesting solutions proposed, in particular shape analysis, separation logic, ownership types and dynamic frames. Few widely used proof environments have integrated these techniques. That may still happen, but the obstacles are significant; in particular, the first two approaches suffer (in our opinion) by attempting to draw a picture of the run-time pointer structure that is more precise than needed for alias analysis; and the last three assume a supplementary annotation effort (in addition to standard Hoare assertions) at which programmers may balk. The theory, calculus and prototype implementation described here strive to avoid these limitations. A representative application is to prove the absence of aliasing between any elements of two linked lists created and modified through typical object-oriented techniques. Assume a standard implementation of lists with an operation to add elements at the end:
However separation logic and shape analysis try to reveal a more detailed structure of pointers than it is necessary for alias analysis REF .
Steps towards a theory and calculus of aliasing
International Journal of Software and Informaticsspecial issue (Festschrift in honor of Manfred Broy), Chinese Academy of Sciences, 2011, pages 77-116
Computer Science