Patterns and Rules for Behavioural Subtyping

Abstract Subtyping relations for object-oriented formalisms describe relationships be-tween super- and subclasses which satisfy the substitutability requirement im-posed on types and their subtypes. Behavioural subtyping is concerned with subtypes for active classes with an explicit dynamic behaviour, specifiable for instance by object-oriented formal methods combining state-based with beha-vioural formalisms. In this paper we develop syntactic patterns and semantic rules for the state-based part of a subclass which guarantee that the subclass is a behavioural sub-type of its superclass. This allows to check for subtypes without computing the behavioural semantics of the class at all. Our results are similar to the ones linking data refinement in state-based methods with failure-divergence refine-ment in CSP. In contrast to classical data refinement, subtyping has to cope with additional new operations in the subclass