Abstract: Objects have been described as having identity, state and
   behaviour, but there are differing views as to what are an object's
   states. For a programmer using an object-oriented programming
   language, the state is the current values of all the attributes,
   hidden and accessible. In most object-oriented design methods, an
   object's state is an abstraction of this: design states are determined
   by the observable behaviour of the object. The difference is
   significant, for example the two views behave differently under
   inheritance, and this can make it difficult to validate an
   implementation against its design specification.
   
   We describe a technique for resolving these different views of state.
   The representation states of an object can be partitioned into
   abstract states by predicates on the attributes. A direct implication
   is that the behaviour of objects can be described by finite state
   machines. Since there are established testing techniques based on
   proving the equivalence of two state machines (for example, a design
   specification and its implementation), it is now feasible to prove
   test coverage, to the level of abstract states, of automatically
   generated tests for object-oriented programs.