June 22, 2010 – 6 years, 9 months ago, by eifler
Illustrate specification and verification techniques on the problem of specifying the behavior of the composite pattern.
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.
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.
This benchmark was taken from the workshop for Specification and Verification of Component-Based Systems SAVCBS'08
The Paper "Speciﬁcation and veriﬁcation challenges for sequential object-oriented programs" by Gary T. Leavens and K. Rustan M. Leino and Peter Müller contains an example implementation of the Composite Design Pattern which can be found in Figure 10.
Timo Eifler firstname.lastname@example.org