Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector

Authors: Daniel Jackson and Craig Damon

Proceedings of the International Symposium on Software Testing and Analysis, January, 1996.

Download the Postscript (approx. 7MB). or PDF

Download the Postscript (approx 800KB, Figs 1 and 2 omitted). or PDF

Abstract

We illustrate the application of a checking tool to the design of a style mechanism for a word processor. The design is cast, along with some expected properties, in a subset of Z that corresponds to the relational calculus. The tool evaluates a property by enumerating all possible cases within some finite bounds, displaying as a counterexample the first case for which the property fails to hold. Unlike animation or execution tools, our checker does not require state transitions to be expressed constructively, and unlike theorem provers, operates completely automatically without user intervention. Using a variety of reduction mechanisms, it can cover an enormous number of cases in a reasonable time, so that quite subtle flaws can be rapidly detected.

Keywords: requirements analysis, design analysis, functional specification, formal specification, Z, relational calculus, model checking, exhaustive testing.

Composable Software Systems Research Group in the School of Computer Science at Carnegie Mellon University.

[Last modified 19-Feb-1999.
Mail suggestions to the Maintainer.]