Contractor Validation Tool

All the files necessary for replaying this case studies are available in the examples section of this web site.

3. ListItr

Class source: JDK 1.4 implementation (Java)
Behaviour requirements source: Manually-generated model by a senior Java developer with 8+ years of experience.

The Java List Iterator (ListItr) provides functionality to go through the elements stored in a List.

It is initialized passing both the target list and the initial index from which the iteration begins. If the end of the list has not been hit, the iterator can retrieve the next element. Conversely, it can retrieve the prev element if the current index is not 0.

The add operation can be invoked at any moment, and it incorporates a new element at the current position. The rem and set methods operate on the last element that has been retrieved: the first one removes it from the list; the other replaces it by another element.

The following abstraction was obtained by Contractor when analysing the JDK 1.4 Java List Iterator implementation over an ArrayList.

Notice that while producing our abstraction Blast was uncertain in a number of transitions, which are suffixed with a “?” symbol. Contractor reported that the cause of this uncertainty is that the invariant may not be preserved. A finer-grained manual analysis revealed that the invariant is not violated, however Blast is not able to prove this.

A senior Java developer with more than 8 years of experience (including experience with formal models) manually generated a behaviour model by analysing the JDK implementation for the list iterator. During this creation process, the developer executed a number of usage scenarios to refine his understanding of the code.

The following is the model that the developer constructed:

When comparing this manually-generated model with our abstraction, the reviewer discovered that:

1. •The overall level of abstraction was comparable to that of enabledness: more than half of the states in the manually-generated model were present in our abstraction.
   

2. •There were 2 states in the manually-generated model which were enabledness-equivalent. This is because the developer decided to separately consider the cases in which the iterated list had exactly one element.
   

3. •There were 3 states in the manually-generated model which were not traceable to states in our abstraction. When further analysing the conditions implied by these states, the reviewer discovered that they were exhibiting spurious behaviour and were accidentaly introduced by the developer, due to his misunderstanding of the requirements.
   

ICSE 2011 Manuscript Case Studies