Eclipse Verification Results

This document shows some results obtained from an experiment we have conducted at Massey University. We have extracted contracts from the Eclipse extension point documentation and in some cases from the documentation of interfaces referenced in extension points, and formalised them using Treaty. We then verified Eclipse against these contracts. The main point we are trying to make is that there is a clear benefit of having formal contracts, and that the current state of the art in Eclipse sometimes leads to violations of the Eclipse house rules (such as the fair play rule). For instance, consider the org.eclipse.help.toc extension point. The extension point documentation contains a DTD that describes the structure of a table of contents document. However, it turns out that many extensions provide toc files not instantiating this DTD. The engineers who implemented those plugins had insider knowledge (of how the plugin is actually consumed by another plugin) and used additional markup. This is also an example of Bertrand Meyer's closet contract conjecture.

The contracts in this documents are just a subset of the contracts we have investigated (1139 component collaborations, 3354 contract instances). We have also used a larger set of Eclipse plugins (the Ganymede EE edition) for our experiment. The full results and the interpretation of the results can be found in a paper that has been submitted for publication.

Another result of our study is that contracts can be rather complex, and that a contract language must be expressive enough to deal with this. In particular, disjunction is needed. Most contracts use basic interface interoperability conditions (Java class - Java interface or XML instance - DTD). However, we have found a few contracts that needed semantic conditions. We have used a modified version of JUnit (with added dependency injection) to express them.

The full list of contracts can be found in the Google code repository. All the code needed to repeat the experiment (including the reporting plugin used to generate the result pages) is in the repository.

Jens Dietrich and Lucia Stewart, 2009

Click on the extension point to see the detailed reports.

extension pointcontract instancesverification failed
net.java.treaty.eclipse.example.clock.dateformatter62
net.java.treaty.eclipse.vocabulary40
org.eclipse.core.expressions.propertyTesters210
org.eclipse.core.resources.markers690
org.eclipse.core.runtime.applications286
org.eclipse.help.contexts3818
org.eclipse.help.toc197
org.eclipse.team.core.fileTypes200
org.eclipse.ui.actionSets241
org.eclipse.ui.bindings230
org.eclipse.ui.commands350
org.eclipse.ui.editorActions150
org.eclipse.ui.handlers173
org.eclipse.ui.keywords280
org.eclipse.ui.perspectiveExtensions190
org.eclipse.ui.propertyPages220