Preventing Cross-Type Aliasing for More Practical Reasoning
				  by
	      Krishna Kishore Dhara and Gary T. Leavens

			       Abstract

To reason about the correctness of a method when cross-type aliases
are possible, one must not only consider all possible patterns of
aliasing among the method's arguments, but all possible ways in which
these types' abstract (specification-only) fields may be aliased.
Because of the large number of such aliasing possibilities, and
because of the complications they cause for reasoning, cross-type
aliases make the use of method specifications impractical in reasoning
about correctness.  Hence, existing work on behavioral subtyping
either ignores aliasing or prohibits the use of method specifications
in reasoning We present a simple type system that prohibits cross-type
aliases, and thus eliminates these problems.  The ``viewpoint
restriction'' enforced by this type system supports a less restrictive
notion of behavioral subtyping -- weak behavioral subtyping.  Weak
behavioral subtyping allows types with immutable objects (e.g.,
immutable sequences), to have behavioral subtypes with mutable objects
(e.g., mutable arrays).  Thus, besides permitting one to reason with
method specifications, the viewpoint restriction also permits a more
flexible and useful notion of behavioral subtyping.


Keywords: Cross-type aliasing, viewpoint restriction, weak
behavioral subtyping, strong behavioral subtyping,
aliasing, mutation, modularity, specification, verification,
Java language, JML language.


2000 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML;
D.2.2 [Software Engineering]
        Design Tools and Techniques --- Object-oriented design methods;
D.2.3 [Software Engineering]
        Coding Tools and Techniques --- Object-oriented programming;
D.2.4 [Software Engineering]
        Software/Program Verification --- Class invariants,
        correctness proofs, formal methods,
        programming by contract, reliability, tools, JML;
D.2.7 [Software Engineering]
	Distribution, Maintenance, and Enhancement --- Documentation;
D.3.2 [Programming Languages]
	Language Classifications --- Object-oriented langauges;
D.3.3 [Programming Languages]
	Language Constructs and Features --- classes and objects,
        inheritance;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, logics of programs,
                pre- and post-conditions,
                specification techniques;

Copyright (c) 2001 by Krishna Kishore Dhara and Gary T. Leavens.