  Relating formal re nement techniques with commercial object oriented software
development methods is important to achieve enhancement of the power and
exibility of these software development methods and tools. We will present an
automata model together with a denotational and an operational semantics to
describe the behavior of objects. Based on the given semantics we de ne a set
of powerful re nement rules and discuss their applicability in software
engineering practice especially with the use of inheritance.
