E.4 New Options in Postconditions

Completely new in version 2.0 is the option to specify that an object has sent messages to other objects during the execution of an operation. The general syntax is: calledObject^calledOperation(params) . To support this, a new OclMessage type has been defined, together with a number of convenience operations:

• isSent

• isSignalSent

• isOperationCall

• hasReturned

• result

Another aspect that can be examined in a postcondition is whether or not an object was created during the execution of the operation. The predefined operation oclIsNew returns true if the object was not in existence at precondition time.