context Subject::hasChanged()
post: observer^update(12,
14)
The observer^update(12, 14) results in true if an update message with arguments 12 and 14 was sent to observer during the execution of the operation. Update() is either an Operation that is defined in the class of observer, or it is a Signal specified in the UML model. The argument(s) of the message expression (12 and 14 in this example) must conform to the parameters of the operation/signal definition.
If the actual arguments of the operation/signal are not known, or not restricted in any way, it can be left unspecified. This is shown by using a question mark. Following the question mark is an optional type, which may be needed to find the correct operation when the same operation exists with different parameter types.
context Subject::hasChanged()
post: observer^update(?
: Integer, ? : Integer)
This example states that the message update has been sent to observer,
but that the values of the parameters are not known.
OCL also defines a special OclMessage type. One can get the
actual OclMessages through the message operator: ^^.
context Subject::hasChanged()
post: observer^^update(12,
14)
This results in the Sequence of messages sent. Each element of the collection is an instance of OclMessage. In the remainder of the constraint one can refer to the parameters of the operation using their formal parameter name from the operation definition. If the operation update has been defined with formal parameters named i and j, then we can write:
context Subject::hasChanged()
post: let
messages : Sequence(OclMessage) = observer^^update(? : Integer, ? : Integer)
in
messages->notEmpty()
and
messages->exists(
m | m.i > 0 and m.j >= m.i )
The value of the parameter i is not known, but it must be greater than zero and the value of parameter j must be larger or equal to i..
Because the ^^ operator results in an instance of OclMessage, the message expression can also be used to specify collections of messages sent to different targets. For an observer pattern we can write:
context Subject::hasChanged()
post: let
messages : Sequence(OclMessage) =
observers->collect(o | o^^update(? : Integer, ? : Integer) ) in
messages->forAll(m
| m.i <= m.j )
Messages is now a set of OclMessage instances, where every
OclMessage instance has one of the observers as a target.
context Person::giveSalary(amount
: Integer)
post: let
message : OclMessage = company^getMoney(amount) in
message.hasReturned()
-- getMoney was sent and returned
and
message.result()
= true -- the getMoney call returned true
As with the previous example we can also access a collection of return
values from a collection of OclMessages. If message.hasReturned()
is false, then message.result() will be undefined.
The Example and Problem
Suppose we have build a component, which takes any form of input and transforms it into garbage (aka encrypts it). The component GarbageCan uses an interface UsefulInformationProvider which must be implemented by users of the component to provide the input. The operation getNextPieceOfGarbage of GarbageCan can then be used to retrieve the garbled data. Figure 4 shows the component's class diagram. Note that none of the operations are marked as queries.
When selling the component, we do not want to give the source code
to our customers. However, we want to specify the component's behavior
as precisely as possible. So, for example, we want to specify, what getNextPieceOfGarbage
does. Note that we cannot write:
context GarbageCan::getNextPieceOfGarbage()
: Integer
post: result
= (datasource.getNextPieceOfData() * .7683425 + 10000) / 20 + 3
because UsefulInformationProvider::getNextPieceOfData() is not a query (e.g., it may increase some internal pointer so that it can return the next piece of data at the next call). Still we would like to say something about how the garbage is derived from the original data.
The solution
To solve this problem, we can use an OclMessage to represent the call to getNextPieceOfData. This allows us to check for the result. Note that we need to demand that the call has returned before accessing the result:
context GarbageCan::getNextPieceOfGarbage()
: Integer
post: let
message : OclMessage = datasource^^getNextPieceOfData()->first() in
message.hasReturned()
and
result
= (message.result() * .7683425 + 10000) / 20 + 3