home · mobile · calendar · defenses · 2003-2004 · 

Thesis Defense - Henkel

Discovering and Debugging Algebraic Specifications for Java Classes
Computer Science PhD Candidate

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.

I 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. I conclude my talk with evaluation results and ideas for future research.

Committee: Amer Diwan, Assistant Professor (Chair)
William Waite, Professor
Alexander Wolf, Professor
Daniel Connors, Assistant Professor
James Martin, Associate Professor
Department of Computer Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
May 5, 2012 (14:20)