Challenge Problem
	SAVCBS'07
	Workshop at ESEC/FSE 2007 September 3-4, 2007

Challenge Problem: Subject-Observer Specification

One session during this year's workshop will be devoted to presenting solutions (full or partial) to the following challenge problem.

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.

To make this concrete, we propose the following two interfaces for the components:

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

interface IObserver {
    void Notify(ISubject s);
}

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.

For our challenge problem session, we invite participants to illustrate their specification and verification techniques on the problem of specifying the behavior of subjects and observers. 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. They should illustrate innovative features of your particular specification or verification techniques. Solutions may be full or partial. The session is open to both presenters and participants of the workshop.

Submission Details

Solutions continue to be accepted as workshop space permits.

Prospective authors should submit their solutions using on-line at http://www.easychair.org/SAVCBS07/. Questions about the challenge problem can be addressed to Mike Barnett (Michael.Barnett@microsoft.com). Submit documents in PDF or PS format, with a maximum length of 6 pages. Solutions will be reviewed by 2 PC members, and if accepted authors will have about 10 minutes (including 3 minutes for questions) to present their solution in the workshop. Solutions will be made available on the SAVCBS web site but will not be part of the proceedings.