Developing and debugging algebraic specifications for Java classes

Research output: Contribution to journalArticle

Abstract

Modern programs make extensive use of reusable software libraries. For example, a study of a number of large Java applications shows that between 17% and 30% of the classes in those applications use container classes defined in the java.util package. Given this extensive code reuse in Java programs, it is important for the interfaces of reusable classes to be well documented. An interface is well documented if it satisfies the following requirements: (1) the documentation completely describes how to use the interface; (2) the documentation is clear; (3) the documentation is unambiguous; and (4) any deviation between the documentation and the code is machine detectable. Unfortunately, documentation in natural language, which is the norm, does not satisfy the above requirements. Formal specifications can satisfy them but they are difficult to develop, requiring significant effort on the part of programmers. To address the practical difficulties with formal specifications, we describe and evaluate a tool to help programmers write and debug algebraic specifications. Given an algebraic specification of a class, our interpreter generates a prototype that can be used within an application like a regular Java class. When running an application that uses the prototype, the interpreter prints error messages that tell the developer in which way the specification is incomplete or inconsistent with a hand-coded implementation of the class. We use case studies to demonstrate the usefulness of our system.

Details

Authors
External organisations
  • University of Colorado
Research areas and keywords

Subject classification (UKÄ) – MANDATORY

  • Software Engineering

Keywords

  • Algebraic interpretation, Algebraic specifications, Specification discovery
Original languageEnglish
Article number14
JournalACM Transactions on Software Engineering and Methodology
Volume17
Issue number3
Publication statusPublished - 2008 Jun 1
Publication categoryResearch
Peer-reviewedYes
Externally publishedYes