Elements of Style: Analyzing a Software Design Feature
with a Counterexample Detector
Authors:Daniel Jackson and Craig A. Damon
International Symposium on Software Testing and Analysis,
Download the PostScript (approx. 7MB).
Download the PostScript (approx 800KB, Figs 1 and 2 omitted).
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.
requirements analysis, design analysis, functional specification,
formal specification, Z, relational calculus, model checking, exhaustive
Back to Nitpick Home Page