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

Subject

Observer

observers *

+ attach(in : Observer)
+ detach(in : Observer)
+notify()

+ update()

for all o in observers
{ o->Update() }

ConcreteSubject
− subjectState
+ setState()
+ getState()

ConcreteObserver
− observerState
+update()

1

subject

observerState =
subject->getState()

return subjectState

Fig. 4. A UML class diagram of the Observer pattern

Structure: The class structure of the Observer pattern is illustrated by the class
diagram in Figure 4. The Observer pattern is modeled with the above mentioned
classes Subject and Observer as abstract classes with a directed association from
Subject to Observer , indicating that the subject is capable of calling the Update
operation on observer objects.The two abstract classes each have a concrete
counterpart, ConcreteSubject and ConcreteObserver , that inherit from the re-
spective abstract classes. Between the ConcreteSubject and ConcreteObserver
classes a directed association towards the ConcreteSubject lets concrete observer
objects call the getState operation on concrete subjects to get its state.

Participants: Subject knows its observers. Any number of observers can observe
a subject. Observer defines an updating interface for objects that should be
notified of changes in a subject. ConcreteSubject stores the state of interest to
the ConcreteObserver and sends a notification to its observers when the state is
changed. The ConcreteObserver maintains a reference to a ConcreteSubject ob-
ject and stores the state of it to stay consistent. A sequence diagram illustrating
interactions of the participants is given in Figure 5.

Verification Conditions for the Observer pattern: The structure of the
Observer pattern, as given in Figure 4, imply a CSP-OZ translation as in Figure
6 which gives the functional verification conditions. The Observer and Subject
classes are both specified as abstract classes with an association that is navigable
form Subject to Observer . The association implies a data structure in a Subject
object containing Observer objects. This is to register the objects that attach