News Archives

Discovering and Debugging Algebraic Specifications for Java Classes

March 22, 2005

  • Date: Tuesday, March 22, 2005 
  • Time: 11:00 a.m. 
  • Place: Woodward 149

Amer Diwan
University of Colorado at Boulder, diwan@cs.colorado.edu
http://www.cs.colorado.edu/~diwan

When a programmer uses a class library, well documented interfaces are critical to avoid bugs. Algebraic specifications can document interfaces unambiguously and accurately, and are thus desirable to augment informal documentation. Unfortunately, algebraic specifications are costly to develop.

We present a system for reducing the cost of developing algebraic specifications for Java classes. The system consists of two components: an algebraic specification discovery tool and an algebraic interpreter. The first tool automatically discovers algebraic specifications from Java classes. The tool generates tests and captures the information it observes during their execution as algebraic axioms. In practice, this tool is accurate, but not complete. Still, the discovered specifications are a good starting point for writing a specification. The second component of our system is the algebraic specification interpreter, which helps developers in achieving specification completeness. Given an algebraic specification of a class, the interpreter generates a rapid prototype which can be used within an application just like any regular Java class. When running an application that uses the rapid prototype, the interpreter prints error messages that tell the developer in which way the specification is incomplete.

This is collaborative work with Johannes Henkel and Christoph Reichenbach.