Special Operators

In the following, let m be the name of the message being specified, T be the sequence of messages sent to the object so far including m and S₁ be the sequence just before m is sent.

• Message expressions - of the form denote values that the message m will return when called with actual parameter values of arg₁, ..., arg_n.

• The ``@'' operator - this specifies that the expression following the ``@'' should be evaluated using S₁ as the sequence for any operator(s) requiring a sequence.

  Consider the following sequence of messages to a Queue object
  
  Queue() Enqueue(10) Dequeue() Enqueue(5)
  
  The value of the expression <tex2html_verb_mark>37<tex2html_verb_mark>enabled(Dequeue) is false for this sequence, whereas the value of enabled(Dequeue) is true.

• The ``enabled'' operator - takes a message and returns true iff extending the current sequence of messages by that message will return normally. A recursive definition of this operator can be given as follows.

  An expression enabled(m) , where m is a message, evaluates to true at T iff

  • m is in the enables clause of m, or
  • m is not in the disables clause of m and @enabled(m) is true.

  Consider the Queue example and the sequence
  
  Queue() Enqueue(10) Dequeue() Enqueue(5)
  
  Here, enabled(Dequeue) is true, whereas <tex2html_verb_mark>40<tex2html_verb_mark>enabled(Dequeue) is false.

• The ``#'' operator - takes a message name. It counts the number of messages in T with the given name that terminated normally.

  Consider the following sequence of messages to a Queue object.
  
  Queue() Dequeue() Enqueue(10)
  
  The value of the expression #(Dequeue) is 0 because the first Dequeue would terminate abnormally.

  On the other hand, consider the sequence
  
  Queue() Dequeue() Enqueue(10) Dequeue()
  
  Here #(Dequeue) evaluates to 1 and so does #(Enqueue).

• The param operator - takes 3 arguments - the number of occurrence of the message name in the sequence T, a message name and a parameter name. An expression param(k, m, n) returns the value of the parameter named n  of the message with name m, in the shortest subsequence T' of T containing m, such that at T', the value of <tex2html_verb_mark>47<tex2html_verb_mark>(m) is k. Value of this expression is undefined if no such (nonempty) T' exists.

  Consider the Queue example and the sequence
  
  Queue() Dequeue() Enqueue(10) Enqueue(5)
  
  At the end of the sequence, the expression param(2, Enqueue, elem) evaluates to 5.

The sequence parameter in the above discussed operators on sequences of messages is implicit. It is always either the current sequence, or the subsequence excluding the last message (when using the ``@'' operator).