Weak Behavioral Subtyping for Types with Mutable Objects

AbstractThis paper studies the question of when one abstract data type (ADT) is a behavioral subtype of another, and proposes a model-theoretic notion of weak behavioral subtyping. Weak behavioral subtyping permits supertype abstraction to be a sound and modular reasoning principle in a language with mutation and limited forms of aliasing. The necessary restrictions on aliasing can be statically checked. Weak behavioral subtyping allows types with mutable objects to be subtypes of types with immutable objects