Design Verification Patterns - Formal Methods and Hybrid Real-Time Systems - page 408

cs:ConcreteSubject

o1:Observer o2:Observer

setState()

notify()

update()

getState()

update()

getState()

Fig. 5. Interactions between the participants in the Observer pattern

themselves as observers. As the classes are declared abstract this is not really
going to be the case, but the concrete ”children” objects, objects of the classes
that inherit from the respective abstract classes have to posses these properties.
The classes ConcreteSubject and ConcreteObserver are the classes that in-
herit from respectively the Subject and Observer classes. The ConcreteObserver
is related to the ConcreteSubject by an association that is navigable towards
the ConcreteSubject . This means that a ConcreteObserver object will have an
attribute of type ConcreteSubject , which store the object to which it is attached.
In [6] the notify operation has a note which says that the operation should
implement a sequential call of the update operation on all attached observers.
The update operation in the Observer class has no attached specification, and do
as such only specify an interface to the concrete observer. Perhaps a use of the
UML interface class to represent the observer would have been more appropriate,
as the update operation is declared as abstract, leaving it to the inheriting classes
to implement the operation body.

Behavioural Verification Condition The original specification of the Observer
pattern do not provide any information on the events of a process encapsulating
the pattern. The behaviour that is guaranteed is

main = Subject.setState

→ Subject.Notify → ( x : o • x .Update → SKIP ); main

The purpose of the observer pattern is as stated to notify observers of state
changes to some subject. This assumption can be analyzed by investigating