This Article 
 Bibliographic References 
 Add to: 
Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector
July 1996 (vol. 22 no. 7)
pp. 484-495

Abstract—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.

[1] R.J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," Proc. Fourth ACM SIGSOFT Symp. Foundations of Software Eng., Oct. 1996.
[2] J.M. Atlee and J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," IEEE Trans. Software Eng., vol. 19, no. 1, pp. 24-40, Jan. 1993.
[3] J.C. Bicarregui, J.S. Fitzgerald, P.A. Lindsay, R. Moore, and B. Ritchie, Proof in VDM: A Practitioner's Guide, Springer-Verlag, Berlin, 1994.
[4] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang., "Symbolic model checking: 1020states and beyond," Information and Computation, vol. 98, no. 2, pp. 142-170, June 1992.
[5] J. Bowen and M.J.C. Gordon, "Z and HOL," Proc. Z User Workshop, pp. 141-167,Cambridge, England, Springer-Verlag Workshops in Computing, 1994.
[6] R. Berghammer and C. Hattensperger, "Computer-Aided Manipulation of Relational Expressions and Formulae Using RALF," Technical Report, Institut fur Informatik und Praktische Mathematik, Christian-Albrechts Universitat Zu Kiel, Germany, 1994.
[7] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[8] E.M. Clarke, T. Filkorn, and S. Jha, “Exploiting Symmetries in Temporal Model Logic Model Checking,” Proc. CAV'93, C. Courcoubetis, ed., pp. 450–462, 1993.
[9] E.M. Clarke, O. Grumberg, and D.E. Long, "Model Checking and Abstraction," Proc. ACM Symp. Principles of Programming Languages, Jan. 1992.
[10] C.A. Damon and D. Jackson, "Efficient Search as a Means of Executing Specifications," Proc. Second Int'l Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96),Passau, Germany, Mar. 1996.
[11] J. Douglas and R.A. Kemmerer, "Aslantest: A Symbolic Execution Tool for Testing ASLAN Formal Specifications," Proc. ISTSTA '94—Int'l Symp. Software Testing and Analysis, ACM Software Engineering Notes, pp. 15-27, 1994.
[12] R. Elmstrøm, P.B. Lassen, and P.G. Larsen, "The IFAD VDM-SL Toolbox, A Practical Approach to Formal Specifications, ACM SIGPLAN Notices, Summer 1994.
[13] M. Engel and J.U. Skakkebaek, "Applying PVS to Z," Technical Report ID/DTU ME 3/1, ProCos Project, Dept. of Computer Science, Technical Univ. of Denmark, Lyngby, Denmark.
[14] S. Garland, J. Guttag, and J. Horning, "Debugging Larch Shared Language Specifications," IEEE Trans. Software Eng., vol. 16, no. 9, pp. 1,044-1,057, Sept. 1990.
[15] J. Guttag and J. J. Horning,“Formal specification as a design tool,”in7th ACM Symp. on Principles of Programming Languages,Las Vegas, NV, Jan. 1980, pp. 251–261.
[16] P. Godefroid, D. Peled, and M. Staskauskas, "Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs," Proc. Int'l Symp. Software Testing and Analysis,San Diego, Calif., pp. 261-269, Jan. 1996.
[17] Specification Case Studies, second edition., I. Hayes, ed., Prentice Hall Int'l (UK) Ltd, 1993.
[18] C.L. Heitmeyer, B.L. Labaw, and D. Kiskis, "Consistency Checking of SCR-style Requirements Specifications," Proc. Int'l Symp. Requirements Engineering, Mar. 1995.
[19] P. Henderson, "Finite State Modelling in Program Development," Proc. Int'l Conf. Reliable Software,Los Angeles, 1975.
[20] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[21] C.N. Ip and D.L. Dill,“Better verification through symmetry,” Proc. 11th Int’l Symp. Computer Hardware Description Languages and Their Applications, pp. 87-100, Apr. 1993.
[22] D. Jackson, "Abstract Model Checking of Infinite Specifications," M. Naftalin, T. Denvir, and M. Bertran, eds., FME'94: Industrial Benefit of Formal Methods, Proc. Second Int'l Symp. Formal Methods Europe, Lecture Notes in Computer Science 873, pp. 519-531,Barcelona, Spain. Springer-Verlag, Oct. 1994.
[23] D. Jackson, "Exploiting Symmetry in the Model Checking of Relational Specifications," Technical Report CMU-CS-94-219, School of Computer Science, Carnegie Mellon Univ., Dec. 1994.
[24] D. Jackson, "Structuring Z Specifications with Views, ACM Trans. on Software Engineering and Methodology, vol. 4, no. 4, pp. 365-389, Oct. 1995.
[25] D. Jackson and C.A. Damon, "Semi-Executable Specifications," Technical Report CMU-CS-95-216, School of Computer Science, Carnegie Mellon Univ., Nov. 1995.
[26] D. Jackson and C.A. Damon, "Nitpick: A Checker for Software Specifications (Reference Manual)," Technical Report CMU-CS-96-109, School of Computer Science, Carnegie Mellon Univ., Jan. 1996.
[27] D. Jackson and M. Jackson, "Problem Decomposition for Reuse," Software Eng. J., Jan. 1996, Vol. 11, No. 1, pp. 19-30.
[28] D. Jackson, S. Jha, and C.A. Damon, "Faster Checking of Software Specifications by Eliminating Isomorphs," Proc. ACM Symp. Principles of Programming Languages,St. Petersburg Beach, Fla., Jan. 1996.
[29] R.B. Jones, "ICL ProofPower," British Computer Soc. Formal Aspects of Computer Science, Series 3, vol. 1, no. 1, pp. 10-13, 1992.
[30] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[31] P.B. Lassen and P.G. Larsen, "An Executable Subset of Meta-IV with Loose Specification," Proc. VDM: Formal Software Development Methods, Noordwijkerhout,Netherlands, Springer-Verlag, Berlin, Oct. 1991.
[32] D. Parnas and J. Madey, "Functional Documentation for Computer Systems Engineering," Technical Report TR-90-287, Queen's Univ., Kingston, Ontario, Sept. 1990.
[33] J.K. Slaney, "Finder: Finite Domain Enumerator, System Description," Proc. 12th Int'l Conf. Automated Deduction, pp. 798-801, Lecture Notes in Artificial Intelligence series, Springer Verlag, Berlin, 1994.
[34] J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, Englewood Cliffs, N.J., 1992.
[35] S.H. Valentine, "Z—, An Executable Subset of Z," Z User Workshop, J.E. Nicholls, ed., York, 1991. Springer-Verlag Workshops in Computing, 1992.
[36] J.C.P. Woodcock and J. Davies, Using Z: Specification, Refinement and Proof. Prentice-Hall, 1996.
[37] J.M. Wing and M. Vaziri-Farahani, “Model Checking Software Systems: A Case Study,” Proc. ACM SIGSOFT Symp. Foundations of Software Eng., 1995.

Index Terms:
Abstract modeling, software design, formal specification, Z notation, model checking, exhaustive testing.
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
Usage of this product signifies your acceptance of the Terms of Use.