Preventing Cross-Type Aliasing for More Practical Reasoning







Deposit Papers 


Dhara, Krishna Kishore and Leavens, Gary T. (2001) Preventing Cross-Type Aliasing for More Practical Reasoning. Technical Report 01-02a, Computer Science, Iowa State University.

Full text available as:Adobe PDF


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
Subjects:Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Coding Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Distribution, Maintenance, and Enhancement
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Classifications
ID code:00000257
Deposited by:Gary T. Leavens on 27 November 2001
Alternative Locations:

Contact site administrator at: