archives

Preventing Cross-Type Aliasing for More Practical Reasoning


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

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
Postscript

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
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:ftp://ftp.cs.iastate.edu/pub/techreports/TR01-02/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR01-02/TR.pdf



Contact site administrator at: ssg@cs.iastate.edu