Elements of style: analyzing a software design feature with a counterexample detector

ABSTRACT

We illustrate the application of Nitpick, a specification checker, 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, 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.

REFERENCES

• BCo95: The B-Technologies: a system for computer aided programming. B-Core (UK) Limited, Oxford, England, 1995.
• AG93: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305]
• BC+90: J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and J. Hwang. Symbolic model checking: 1020 states and beyond. Proc. 5th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, June 1990.
• CES86: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• CFJ93: Edmund M. Clarke , Thomas Filkorn , Somesh Jha, Exploiting Symmetry In Temporal Logic Model Checking, Proceedings of the 5th International Conference on Computer Aided Verification, p.450-462, June 28-July 01, 1993
• DK94: Jeffrey Douglas , Richard A. Kemmerer, Aslantest: a symbolic execution tool for testing Aslan formal specifications, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.15-27, August 17-19, 1994, Seattle, Washington, United States [doi>10.1145/186258.186487]
• ELL94: René Elmstrøm , Peter Gorm Larsen , Poul Bøgh Lassen, The IFAD VDM-SL toolbox: a practical approach to formal specifications, ACM SIGPLAN Notices, v.29 n.9, p.77-80, Sept. 1994 [doi>10.1145/185009.185028]
• GGH90: S. J. Garland , J. V. Guttag , J. J. Horning, Debugging Larch Shared Language Specifications, IEEE Transactions on Software Engineering, v.16 n.9, p.1044-1057, September 1990 [doi>10.1109/32.58789]
• GH80: John Guttag , J. J. Horning, Formal specification as a design tool, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.251-261, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567471]
• Hei95: C. Heitmeyer , B. Labaw , D. Kiskis, Consistency checking of SCR-style requirements specifications, Proceedings of the Second IEEE International Symposium on Requirements Engineering, p.56, March 27-29, 1995
• ID93: C. Norris Ip , David L. Dill, Better Verification Through Symmetry, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.97-111, April 26-28, 1993
• Jac94a: Daniel Jackson, Abstract Model Checking of Infinite Specifications, Proceedings of the Second International Symposium of Formal Methods Europe on Industrial Benefit of Formal Methods, p.519-531, October 24-18, 1994
• Jac94b: Daniel Jackson, Exploiting Symmetry in the Model Checking of Relational Specifications, Carnegie Mellon University, Pittsburgh, PA, 1994
• JJ96a: Daniel Jackson , Somesh Jha , Craig A. Damon, Faster checking of software specifications by eliminating isomorphs, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.79-90, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237733]
• JJ96b: Daniel Jackson and Michael Jackson. Problem Decomposition for Reuse. to appear, Software Engineering }ournal, (special issue on viewpoints).
• LH+94: Nancy G. Leveson , Mats Per Erik Heimdahl , Holly Hildreth , Jon D. Reese, Requirements Specification for Process-Control Systems, IEEE Transactions on Software Engineering, v.20 n.9, p.684-707, September 1994 [doi>10.1109/32.317428]
• LL91: Peter Gorm Larsen , Poul Bøgh Lassen, An Executable Subset of Meta-IV with Loose Specification, Proceedings of the 4th International Symposium of VDM Europe on Formal Software Development-Volume I: Conference Contributions, p.604-618, October 21-25, 1991
• PM90: D. Parnas and j. Madey. Functional documentation for computer systems engineering. Technical Report TR-90-287, Queen's University, Kingston, Ontario, September 1990.
• Spi89: J. M. Spivey, The Z notation: a reference manual, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• Val91: Samuel H. Valentine, Z--, an Executable Subset of Z, Proceedings of the Z User Workshop, p.157-187, December 16-17, 1991
• WV95: Jeannette M. Wing , Mandana Vaziri-Farahani, Model checking software systems: a case study, Proceedings of the 3rd ACM SIGSOFT symposium on Foundations of software engineering, p.128-139, October 12-15, 1995, Washington, D.C., United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Verification