An automated tool for analyzing completeness of equational specifications

ABSTRACT

Books on software engineering methodologies talk about the significance and need for designing consistent and complete specifications during the requirement analysis and design stages of a software development cycle. There is, however, little (or at best very limited) discussion of methods for ensuring these structural properties of specifications. In this paper, we discuss methods for checking completeness of equational specifications. Some of these methods were earlier proposed in somewhat different form in the context of developing the so-called inductionless induction method for automating proofs by induction using completion procedures. These methods are implemented in our theorem prover Rewrite Rule Laboratory (RRL), and have been tried on a number of examples of specifications of data abstractions. In case a specification is incomplete, these methods can aid in making them complete by generating templates which are not specified. Templates can also be helpful in distinguishing between intentional and unintentional incompleteness in specifications. Further, these methods can be used to generate test cases for checking specifications and verifying implementations of specifications. These methods are illustrated on examples which exhibit their power as well as limitations.

REFERENCES

• 1: J. A. Bergstra , Jan Heering , Paul Klint, Algebraic specification, ACM Press, New York, NY, 1989
• 2: Valdis Berzins , Lucia Luqi, Software engineering with abstractions, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1991
• 3: L Bougé , N Choquet , L Fribourg , M C Gaudel, Test sets generation from algebraic specifications using logic programming, Journal of Systems and Software, v.6 n.4, p.343-360, Nov. 1986 [doi>10.1016/0164-1212(86)90004-X]
• 4: D. Craigen, S. Gerhart, T. Ralston, An international survey of industrial applications of formal methods. NISTGCR 93/626, National Institute of Standards and Technology, Gaithersburg, MD.
• 5: Richard Fairley, Software engineering concepts, McGraw-Hill, Inc., New York, NY, 1985
• 6: John Gannon , Paul McMullin , Richard Hamlet, Data Abstraction, Implementation, Specification, and Testing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.3, p.211-223, July 1981 [doi>10.1145/357139.357140]
• 7: Carlo Ghezzi , Mehdi Jazayeri , Dino Mandrioli, Fundamentals of software engineering, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 8: John Vogel Guttag, The specification and application to programming of abstract data types., 1975
• 9: J. Guttag and J.J. Horning, "The algebraic specification of abstract data types," Acta Informatica, 10, 27- 52, 1978.
• 10: 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]
• 11: I. Van Horebeek , J. Lewi, Algebraic Specifications in Software Engineering, Springer-Verlag New York, Inc., New York, NY, 1989
• 12: Pankaj Jalote, Testing the Completeness of Specifications, IEEE Transactions on Software Engineering, v.15 n.5, p.526-531, May 1989 [doi>10.1109/32.24701]
• 13: Jean-Pierre Jouannaud , Emmanuel Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, v.82 n.1, p.1-33, July 1989 [doi>10.1016/0890-5401(89)90062-X]
• 14: D. Kaput, "Specification and verification of constructible data structures," Manuscript under preparation.
• 15: Deepak Kapur , Paliath Narendran , Daniel J. Rosenkrantz , Hantao Zhang, Sufficient-completeness, ground-reducibility and their complexity, Acta Informatica, v.28 n.4, p.311-350, April 1991 [doi>10.1007/BF01893885]
• 16: Deepak Kapur , Paliath Narendran , Hantao Zhang, Automating inductionless induction using test sets, Journal of Symbolic Computation, v.11 n.1-2, p.83-111, Jan./Feb. 1991 [doi>10.1016/S0747-7171(08)80133-2]
• 17: D. Kaput, P. Narendran and H. Zhang, "On sufficientcompleteness and related properties of term rewriting systems," Acta In/ormatica 24, 395-415 1987.
• 18: D. Kapur and X. Nie, "Reasoning about numbers in Tecton," Department of Computer Science Technical Report, March 1994. Accepted for presentation at IS- MIS'9d, October 1994.
• 19: D. Kapur and M. Subramaniam, "Automated reasoning about parallel algorithms using powerlists," Manuscript under preparation.
• 20: Deepak Kapur , Hantao Zhang, An Overview of Rewrite Rule Laboratory (RRL), Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, p.559-563, April 03-05, 1989
• 21: R.A. Kemmerer, "Testing formal specifications to detect design errors," {EEE Trans. on Software Engg., 11(1), Jan. 1985, 32-43.
• 22: D. Knuth and P. Bendix, "Simple word problems in universal algebras," in Computational Problems in Abstract Algebra (ed. Leech), Pergamon Press, 263-297, 1970.
• 23: E. Kounalis and H. Zhang, "A general completeness test for equational specifications," Proc. of Hungarian Conference of Computer Science. Also available as Technical Report {85-R-05}, GRIN, Nancy, France, Jan. 1985.
• 24: Jayadev Misra, Powerlist: a structure for parallel recursion, A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1994
• 25: David R. Musser , Deepak Kapur, Rewrite Rule Theory and Abstract Data Type Analysis, Proceedings of the European Computer Algebra Conference on Computer Algebra, p.77-90, April 05-07, 1982
• 26: Tobias Nipkow , Gerhard Weikum, A decidability result about sufficient-completeness of axiomatically specified abstract data types, Proceedings of the 6th GI-Conference on Theoretical Computer Science, p.257-268, January 05-07, 1983
• 27: Roger S. Pressman, Software engineering (3rd ed.): a practitioner's approach, McGraw-Hill, Inc., New York, NY, 1992
• 28: I. Sommerville, Software engineering (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1985
• 29: James Rumbaugh , Michael Blaha , William Premerlani , Frederick Eddy , William Lorensen, Object-oriented modeling and design, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 30: Jean Jacques Thiel, Stop losing sleep over incomplete data type specifications, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.76-82, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800518]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Design, Reliability, Theory