Composite Pattern 2

March 8, 2011 – 6 years ago, by sarahgrebing

Short Description

Specification and verification of the behavior of the composite pattern.


void update(int v) {
 int diff = v val;
 val = v;
 for (CompositeNode p = this; p != null; p = p.parent) {
  p.sum = p.sum + diff;

The signature of the class is:

class CompositeNode {
 CompositeNode parent;
 CompositeNode left, right;
 int val, sum;
 static CompositeNode create(int v);
 void addChild(CompositeNode child); // connect ’this’ as the parent of ’child’
 void dislodge(); // disconnect ’this’ from its parent
 void update(int v);

void compositeHarness()

 CompositeNode a = create(5), b = create(7);
 assert(a.sum == 12);
 assert(a.sum == 22);
 CompositeNode c = create(10);
 b.addChild(c); b.dislodge();
 assert(b.sum == 27);


Long Description

This benchmark, which has been used as a specification and verification challenge at
SAVCBS 2008 [1], involves a set of nodes connected acyclicly via parent links. In addition to graph structure information, each node stores an integer val as well as the sum of the val fields in the tree rooted at the node. The key is to keep these sum fields up-to-date.
A client is allowed access to any node in the set. That is, clients can hold pointers to any node. When the value of a node is updated, all relevant sum fields must be updated as well. This can be accomplished using recursion or by a loop like shown the method update.

In the signature of the class, we have limited nodes to two children, but programs are also allowed to support an unbounded number of children. The precondition of addChild() should prevent cycles from being created and prevent a node from getting more children than the implementation supports. Method dislodge() severs a node’s tie to its parent. All methods must keep all sum fields up-to-date.

It is allowed to modify the specification above to introduce an “manager” object to keep track of disjoint trees of composites.

Verification Tasks

  1. Verify correctness of the harness. 80 points.

Supplementary Materials

The former problem description of [1] can also be found in this collection.
The paper from which this benchmark is taken was published in may 2010 by K. Rustan M. Leino and Michal Moskal. It contains some more benchmarks which are also included on this site.
Information about the scoring system and the pseudo-code description of the programs can be found here.

Submitted by

Sarah Grebing