Validation Code for a Message Declaration

Every message declaration with a behavior description is translated into a code which has a generic part that does the general book-keeping of storing parameters, return values and/or exceptions and a specific part that implements the behavior specification. Below, we discuss the specific part related to implementing the behavior specification.

The specific part has 3 methods (or functions) - enabled, interpretation, isNormal corresponding to the enables/disables, interpretations and the defined by clauses, respectively, of a specification. These methods are for validating subsequent messages, and they are defined below :

• isNormal returns true if the predicate for normal given in the specification evaluates to true and false if the predicate for abnormal evaluates to true. It throws an error if neither normal nor abnormal predicate evaluates to true. Note that this error is different from the exceptions that can be raised by a message sent to the interface.

• enabled takes a message name and a vector of parameters and returns true if the message formed using the name and parameter values is enabled subsequently to the current message as per the enables/disables clauses.

• interpretation takes a message name, a vector of parameters, and a return value and returns true only if that combination of message name, parameter values and return value satisfies the predicate given in the interpretations clauses of the specification for this message.

The specific part also has a boolean method validate that first checks if the message, given the history, behaves as expected. It raises an error, indicating a failure of the test if

• either it is enabled after the last message before this and isNormal returns false, or
• it is not enabled after the last message before this and the method isNormal returns true, or
• the value returned does not satisfy the predicate for the interpretation when evaluated in the previous history.

The IBDL expressions used in the predicates are translated accordingly so that the above methods can be evaluated. A part of the generated class for the Account interface as specified in Section 2 is given in Fig. 2.