Subject-Observer Pattern

June 22, 2010 – 6 years, 10 months ago, by eifler

Short Description

Illustrate specification and verification techniques on the problem of specifying the behavior of subjects and observers.

Code

interface ISubject {
    void Register(IObserver o);
    void Update(Value v);
    Value Get();
}

interface IObserver {
    void Notify(ISubject s);
}

Specification

Long Description

A common programming pattern is to separate the component that encapsulates some state from the components that access that state. The former component is often called a subject, while the latter type is an observer. At a minimum, a subject has a method for registering an observer, a method for updating the encapsulated state, and a method for retrieving the value of the state. Observers must provide a method for being notified: the behavior of the pair is that upon the update method being called, all registered observers have their notification method called.

There may be many observers for a subject and an observer may be registered with more than one subject. Thus the notification method takes as a single parameter a reference to the subject so the observer knows which subject’s retrieval method should be called if it is interested in the new value of the subject’s state. A common constraint is that during the period a subject is calling the notification methods of all registered observers, no further state changes are allowed. Another common constraint is that each observer is called at most once per state change.

Solutions should be clear as to the assumptions made (e.g., sequential programs vs. multi-threaded programs), the level of annotation required, any restrictions (e.g. aliasing) that the technique imposes on code, and the difficulty and amount of automation used in the verification.

Supplementary Materials

This benchmark was taken from the workshop for Specification and Verification of Component-Based Systems SAVCBS'07

Submitted by

Timo Eifler verifythis@cost-ic0701.org