archives

Mutation, Aliasing, Viewpoints, Modular Reasoning, and Weak Behavioral Subtyping


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Dhara, Krishna Kishore and Leavens, Gary T. (2001) Mutation, Aliasing, Viewpoints, Modular Reasoning, and Weak Behavioral Subtyping. Technical Report 01-02, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

Abstract

Existing work on behavioral subtyping either ignores aliasing or restricts the behavior of additional methods in a subtype and only allows one to use invariants and history constraints in reasoning. This prevents many useful subtype relationships; for example, a type with immutable objects (e.g., immutable sequences), cannot have a behavioral subtype with mutable objects (e.g., mutable arrays). Furthermore, the associated reasoning principle is not very useful, since one cannot use the pre- and postconditions of methods. Weak behavioral subtyping permits more behavioral subtype relationships, does not restrict the behavior of additional methods in subtypes, and allows the use of pre- and postconditions in reasoning. The only cost is the need to restrict aliases so that objects cannot be manipulated through the view of more than one type.

Keywords:Weak behavioral subtyping, strong behavioral subtyping, viewpoint, aliasing, mutation, modularity, specification, verification, Java language, JML languag
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): Software/Program Verification (F.3.1)
Software: PROGRAMMING LANGUAGES: Language Classifications
ID code:00000237
Deposited by:Gary T. Leavens on 23 March 2001
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/01-02/TR.ps.gz



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