The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.07 - July (1996 vol.22)
pp: 484-495
ABSTRACT
<p><b>Abstract</b>—We demonstrate how Nitpick, a specification checker, can be applied 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. Nitpick checks 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, Nitpick does not require state transitions to be expressed constructively, and unlike theorem provers, Nitpick 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 subtle flaws can be rapidly detected.</p>
INDEX TERMS
Abstract modeling, software design, formal specification, Z notation, model checking, exhaustive testing.
CITATION
Daniel Jackson, Craig A. Damon, "Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector", IEEE Transactions on Software Engineering, vol.22, no. 7, pp. 484-495, July 1996, doi:10.1109/32.538605
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool