++, etc.) for object-oriented
systems is proposed
based on the message-passing paradigm. Signatures of messages are
enhanced to include semantic information, expressing behavior
clients can expect from a server. Formulas are given to
disambiguate normal termination from abnormal termination of a
message using the return values and exceptions to reflect whether
the pre-condition associated with the message is satisfied or
not. State changes caused by a message invocation are specified
by explicitly enumerating subsequent messages that a message
invocation enables (and/or) disables, by establishing (or
violating, respectively) their pre-conditions. Special operators
on sequences of messages are defined to specify such semantic
information. A specification language IBDL, Interface Behavior
Description Language, based on this methodology is developed.
As IBDL specifications explicitly capture the interactions between
messages, they are ideal for validating implementation behaviors
with sequences of messages.
We present a scheme for sequence testing by translating IBDL
specifications into code.