Discovering documentation for Java container classes

Research output: Contribution to journalArticle


Modern programs make extensive use of reusable software libraries. For example, we found that 17% to 30% of the classes in a number of large Java applications use the container classes from the java.util package. Given this extensive code reuse in Java programs, it is important for the reusable interfaces to have clear and unambiguous documentation. Unfortunately, most documentation is expressed in English, and therefore does not always satisfy these requirements. Worse yet, there is no way of checking that the documentation is consistent with the associated code. Formal specifications present an alternative which does not suffer from these problems; however, formal specifications are notoriously hard to write. To alleviate this difficulty, we have implemented a tool which automatically derives documentation in the form of formal specifications. Our tool probes Java classes by invoking them on dynamically generated tests and captures the information observed during their execution as algebraic axioms. While the tool is not complete or correct from a formal perspective we demonstrate that it discovers many useful axioms when applied to container classes. These axioms then form an initial formal documentation of the class they describe.


External organisations
  • Google Inc.
  • University of Colorado
Research areas and keywords

Subject classification (UKÄ) – MANDATORY

  • Software Engineering


  • Algebraic specifications, Program documentation, Specification inference
Original languageEnglish
Pages (from-to)526-543
Number of pages18
JournalIEEE Transactions on Software Engineering
Issue number8
Publication statusPublished - 2007 Aug 1
Publication categoryResearch
Externally publishedYes