ACM SIGSOFT 2008/FSE 16
November 9-10, 2008
|
|
Challenge Problem for |
| SAVCBS'08 | |
| Workshop at ACM SIGSOFT 2008/FSE 16 November 9-10, 2008 |
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 the composite pattern. A composite object is one that organizes objects into a tree structure in order to represent a part-whole hierarchy. The point of the pattern is that clients have a uniform interface whether they have a reference to a sub-tree (i.e., a composite object) or a leaf (a single object). The focus of the challenge problem is to specify (and verify?) the kind of internal invariant that an implementation of a composite might have.
Consider the class, Composite, that wishes to keep the simplest invariant: that each object, c, of type Composite has a count of the number of objects within the sub-tree rooted at c. Therefore, whenever a component is added as a child of c all of c's ancestors must have their count updated. While c can own (using any of the various ownership methodologies) its children, it cannot own its parent. Yet adding a child to c risks invalidating its parent's invariant.
For our challenge problem session, we invite participants to illustrate their specification and verification techniques on the problem of specifying the behavior of the composite pattern. 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.
Solutions will continue to be accepted as workshop space permits. Prospective authors should submit their solutions on-line at http://www.easychair.org/conferences/?conf=savcbs08. 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 and will be part of the proceedings. Note that publication at SAVCBS will not preclude submitting the same work elsewhere.