Termination Classification

Classify the termination of a message by defining the predicates

• normal  which is true, if the message terminates without raising any exception and possibly returning a value.
• abnormal , which is false, if the message terminates raising an exception.

normal should always be the negation of abnormal. If a message scheme does not raise any exception, then abnormal defaults to false and normal defaults to true.

The IBDL syntax for specifying this is :

(abnormal | normal) defined by expression

The defined by clause is optional. If it is not given, then abnormal defaults to



where e₁, ..., e_k are different exceptions specified in the message scheme. In that case, normal defaults to not(abnormal).

The message can affect the behavior of different sets of messages depending on whether it terminates normally or abnormally. The subsequent specification (of effects of the message) have to be labeled as normal or abnormal. In the current language we don't allow updates in case of abnormal termination, but we might relax this later if we find the need for it.