The Model

In our model, every object has an associated sequence of messages sent to it since its creation. A handle to an object can be obtained by clients using the constructors specified in the interface and the only interactions between a client and an object are through the messages provided in the interface. The first message in every sequence is a successful constructor message that defines (a handle to) the object to which all the subsequent messages are sent.

Every message has a name and a value for each of its parameters. We also assume that given a sequence of messages (to an object), one can count the number of occurrences of messages with a given message name and can access the parameter values of a message in a sequence.

Throughout this section we assume that T is the sequence of messages sent so far to the object, with the first message being a constructor message that uniquely defines the object.