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

Subject
method attach, detach [ o ?: Observer ]
chan update
local chan notify

ConcreteSubject
inherit Subject
method setState [ s ?: O ]
method getState [ s !: O ]

observers : P Observer

subjectState : O

Init
observers = ∅

com setState
Δ ( subjectState )
s ?: O

com attach
Δ ( observers )
o ?: Observer

subjectState = s ?

com getState
Δ ()
s !: O

observers = observers ∪ o ?

com detach
Δ ( observers )
o ?: Observer

s ! = subjectState

enable notify
s ?

observers = observers\{o ? }

s ? = subjectState

effect notify
Δ ()
observers :

P Observer

ConcreteObserver
inherit Observer
chan getState [ s ?: O ]

∀ x ∈ observers • update.x

Observer
method update

subject : ConcreteSubject
observerState : O

com update
Δ ( observerState )
subject : ConcreteSubject

observerState = getState.subject

Fig. 6. The structure of the observer pattern as CSP-OZ schemata

possible method call sequences. For observers o 1 ,...,o n and a concrete subject
object cs a state change must be recognized as following sequence:

cs.Attach ( o 1 ); cs.Attach ( o 3 ); ... ;
cs.setState (); cs.Notify (); o 1 .Update (); o 2 .Update (); ....