Invariants of Complex Object Structures

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

Short Description

Develop a specification and verification technique for invariants of complex object structures.

Code

class Component {
   protected /*@ spec_public @*/ Composite parent;
   protected int total = 1;
   
   //@ protected invariant 1 <= total;
}

class Composite extends Component {
   private Component[] components = new Component[5];
   private int count;
   
   //@ private invariant total == 1 + (\sum int i; 0 <= i && i < count; components[i].total);
   
   //@ requires c.parent == null;
   public void addComponent(Component c) {
      // resize array if necessary
      components[count] = c;
      count++;
      c.parent = this;
      addToTotal(c.total);
   }

   //@ requires 0 <= p;
      private /*@ helper @*/ void addToTotal(int p) {
      total += p;
      if(parent != null) { parent.addToTotal(p); }
   }
}

An implementation of the Composite pattern. As expressed by the JML invariant in Composite, the total field stores the number of (sub-)components of a component. For simplicity, we omit the invariants that express that each component is correctly linked to its parent. The invariant shown in Composite uses nsum to express the addition of all component totals. Method addToTotal is declared as helper, which means that it cannot assume and need not preserve any invariants.

Specification

Long Description

Almost all interesting data structures consist of several interacting objects. The invariant of such a data structure relates the state of several objects, which implies that modifications of these objects potentially affect the invariant. Consequently, a sound verification technique has to generate proof obligations for all methods that modify an object of the data structure to maintain the invariant.
We illustrate invariants of object structures by the implementation of the Composite Pattern in the example above. Each Composite object stores references to its direct sub-components in an array. The invariant of a Composite object x expresses that the field x.total contains the number of components of the composite tree rooted in x. Therefore, the invariant of x depends on the state of x , the array x.components, and the state of x’s direct sub-components. Any method that modifies any of these objects potentially violates x’s invariant. Therefore, the invariant leads to proof obligations for the methods of Component and its subclasses, methods of Composite, and any method that has access to the components array. To handle the latter group of methods in a modular way, one has to employ some form of alias control to limit this group, for instance, to the methods of Composite.
The example illustrates that reasoning about invariants of object structures has to deal with the complications of subclassing and aliasing, and is, therefore, a rather difficult challenge.

Supplementary Materials

The paper by Gary T. Leavens and K. Rustan M. Leino and Peter Müller from which this challenge is taken contains some additional information including references to relevant papers related to this challenge. Some more specification and verification challenges which are also included on this site can also be found there.

Submitted by

Timo Eifler verifythis@cost-ic0701.org