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

Authors:Daniel Jackson and Craig A. Damon

Published in: International Symposium on Software Testing and Analysis, January 1996.

Download the PostScript (approx 800KB, Figs 1 and 2 omitted).

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.

Back to Nitpick Home Page