This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automatically Checking an Implementation against Its Formal Specification
January 2000 (vol. 26 no. 1)
pp. 55-69

Abstract—We propose checking the execution of an abstract data type's imperative implementation against its algebraic specification. An explicit mapping from implementation states to abstract values is added to the imperative code. The form of specification allows mechanical checking of desirable properties such as consistency and completeness, particularly when operations are added incrementally to the data type. During unit testing, the specification serves as a test oracle. Any variance between computed and specified values is automatically detected. When the module is made part of some application, the checking can be removed, or may remain in place for further validating the implementation. The specification, executed by rewriting, can be thought of as itself an implementation with maximum design diversity, and the validation as a form of multiversion-programming comparison.

[1] A.L. Ambler, D.I. Good, J.C. Browne, W.F. Burger, R.M. Cohen, C.G. Hoch, and R.E. Wells, “Gypsy: A Language for Specification and Implementation of Verifiable Programs,” Language Design for Reliable Software, pp. 1-10, 1977.
[2] S. Anantharaman, J. Hsiang, and J. Mzali, “SbReve2: A Term Rewriting Laboratory with (AC-)Unfailing Completion” Proc. RTA '89, pp. 533-537, 1989.
[3] S. Antoy, P. Forcheri, and M.T. Molfino, “Specification-Based Code Generation,” Proc. 23rd Hawaii Int'l Conf. System Sciences, pp. 165-173, Jan. 1990.
[4] S. Antoy and J. Gannon, “Using Term Rewriting Systems to Verify Software,” IEEE Trans. Software Eng., vol. 20, no. 4, pp. 259-274, Apr. 1994.
[5] S. Antoy, P. Forcheri, J. Gannon, and M.T. Molfino, “Equational Specifications: Design, Implementation, and Reasoning,” Advances in the Design of Symbolic Computation Systems A. Miola and M. Temperini, eds., pp. 126-144, Springer, 1996.
[6] A.W. Appel, J.S. Mattson, and D.R. Tarditi, A Lexical Analyzer Generator for Standard ML. Princeton Univ., Dec. 1989.
[7] A.W. Appel, J.S. Mattson, and D.R. Tarditi, ML-Yacc version 2. 0. School of Computer Science, Carnegie Mellon Univ., Pittsburgh, Pa., Apr. 1990.
[8] K. Arnold and J. Gosling, The Java Programming Language, Addison-Wesley, Reading, Mass., 1996.
[9] A. Avizienis and J. Kelly, “Fault Tolerance by Design Diversity: Concepts and Experiments,” Computer, vol. 17, pp. 67-80, 1984.
[10] A. Babbitt, S. Powell, and R. Hamlet, “Prototype Testing Tools,” Technical Report TR90-8, Portland State Univ., Ore., 1990.
[11] V.R. Basili and R.W. Selby, “Comparing the Effectiveness of Software Testing Strategies,” IEEE Trans. Software Eng., vol. 13, pp. 1,278-1,296, 1987.
[12] F. Boinck and H. Van Tilborg, “Constructions and Bounds for Systematic$t$-EC/AUED Codes,” IEEE Trans. Information Theory, vol. 36, no. 6, pp. 1,381-1,390, Nov. 1990.
[13] Algebraic System Specification and Development, M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas and D. Sannella, eds. Springer-Verlag, 1991.
[14] L. Bouge, N. Choquet, L. Fribourg, and M.-C. Gaudel, “Application of Prolog to Test Sets Generation for Algebraic Specifications,” TAPSOFT, pp. 261-275, Springer-Verlag, 1985.
[15] N. Choquet, “Test Data Generation Using a Prolog with Constraints,” Proc. Workshop Software Testing, pp. 132-141, 1986.
[16] W.F. Clocksin and C.S. Mellish,Programming in Prolog, 2nd ed. New York: Springer-Verlag, 1984.
[17] M.D. Davis and E.J. Weyuker, “A Formal Notion of Program-Based Test Data Adequacy,” Information and Control, vol. 56, pp. 52-71, 1983.
[18] N. Dershowitz, “Termination,” RTA '85, pp. 180-223, May 1985.
[19] N. Dershowitz, M. Okada, and G. Sivakumar, “Confluence of Conditional Term Rewrite Systems,” CTRS '87, pp. 31-44, 1987.
[20] R.-K. Doong and P. Frankl, “Case Studies on Testing Object-Oriented Programs,” Proc. Symp. Testing, Analysis, and Verification (TAV4), pp. 165-177, 1991.
[21] M. Ehrig and B. Mahr, Fundamentals of Algebraic Specification 1. Berlin: Springer-Verlag, 1985.
[22] J. Gannon, R. Hamlet, and P. McMullin, “Data Abstraction Implementation, Specification, and Testing,” ACM Trans. Programming Languages and Systems, vol. 3, pp. 211-223, 1981.
[23] J.D. Gannon, R.G. Hamlet, and H.D. Mills, “Theory of Modules,” IEEE Trans. Software Eng., vol. 13, 1987.
[24] M.-C. Gaudel and B. Marre, “Generation of Test Data from Algebraic Specifications,” Proc. Second Workshop Software Testing, Verification, and Analysis, pp. 138-139, 1988.
[25] S. Gerhart, “Test Generation Method Using Prolog” Technical Report TR 85-02, Wang Inst. of Graduate Studies, 1985.
[26] J. Goguen, J.-P. Jouannaud, and J. Meseguer, “Operational Semantics of Order-Sorted Algebras,” Proc. CALP '85, W. Brauer, ed., 1985.
[27] J.A. Goguen, J.W. Thatcher, and E.G. Wagner, “An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types,” Current Trends in Programming Methodology, R.T. Yeh, ed., vol. 4, pp. 80-149. Englewood Cliffs, N.J.: PrenticeHall, 1978.
[28] J.A. Goguen and T. Winkler, “Introducing Obj3,” Technical Report SRI-CSL-88-9, SRI Int'l, Menlo Park, Calif., 1988.
[29] J.V. Guttag and J.J. Horning, “The Algebraic Specification of Abstract Data Types,” Acta Informatica, vol. 10, pp. 27-52, 1978.
[30] J.V. Guttag, J.J. Horning, and J.M. Wing, “The Larch Family of Specification Languages,” IEEE Software, pp. 24-36, Sept. 1985.
[31] J.V. Guttag, E. Horowitz, and D. Musser, “Abstract Data Types and Software Validation,” Comm. ACM, vol. 21, pp. 1,048-1,064, 1978.
[32] D. Hamlet, “Random Testing,” Encyclopedia of Software Eng., J. Marciniak, ed., pp. 970-978. New York: Wiley, 1994.
[33] D. Hamlet and R. Taylor, "Partition Testing Does Not Inspire Confidence," IEEE Trans. Software Eng., vol. 16, pp. 1,402-1,412, Dec. 1990.
[34] R.G. Hamlet, “Testing Programs with the Aid of a Compiler,” IEEE Trans. Software Eng., vol. 3, pp. 279-290, 1977.
[35] C.A.R. Hoare, “Proof of Correctness of Data Representations,” Acta Informatica, vol. 1, pp. 271-281, 1972.
[36] D. Hoffman, “Hardware Testing and Software ICs,” Proc. Pacific Northwest Software Quality Conf., pp. 234-244, 1989.
[37] D. Hoffman and C. Brealey, “Module Test Case Generation,” Proc. Third Symp. Software Testing, Analysis, and Verification, pp. 97-102, 1989.
[38] W. Howden, “Methodology for the Generation of Program Test Data,” IEEE Trans. Computers, vol. 24, pp. 554-559, 1975.
[39] G. Huet, "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems," J. ACM, vol. 27, no. 4, pp. 797-821, Oct. 1980.
[40] S.C. Johnson, “YACC: Yet Another Compiler Compiler,” UNIX Programmer's Manual, vol. 2, pp. 388-400. New York: Holt, Reinhart, Winston, 1983.
[41] J.W. Klop, “Term Rewriting Systems,” Technical Report CS-R9073, Stichting Mathematisch Centrum, Amsterdam, 1990.
[42] J.C. Knight and N.G. Leveson, "An Experimental Evaluation of the Assumption of Independence in Multiversion Programming," IEEE Trans. Software Eng., Vol. 12, No. 1, 1986, pp. 96-109.
[43] D.E. Knuth and P.B. Bendix, “Simple Word Problems in Universal Algebras,” Computational Problems in Abstract Algebras, J. Leech, ed., pp. 263-297. New York: Pergamon Press, 1970.
[44] M.E. Lesk and E. Schmidt, “Lex—A Lexical Analyzer Generator,” UNIX Programmer's Manual, vol. 2, pp. 353-387. New York: Holt, Reinhart, Winston, 1983.
[45] N.G. Leveson, S.S. Cha, and J.C. Knight, T.J. Shimeall, “The Use of Self Checks and Voting in Software Detection: An Empirical Study,” IEEE Trans. Software Eng., vol. 16, pp. 432-443, 1990.
[46] R. London personal communication, Feb. 1991.
[47] D. C. Luckham,Programming with Specifications: An Introduction to Anna, a Language for Specifying Ada Programs. New York: Springer-Verlag, 1990.
[48] B. Meyer,Object-Oriented Software Construction. Englewood Cliffs, NJ: Prentice-Hall, 1988.
[49] J.D. Musa,A. Iannino,, and K. Okumoto,Software Reliability: Measurement, Prediction and Application.New York: McGraw-Hill, 1987.
[50] S. Ntafos, “A Comparison of Some Structural Testing Strategies,” IEEE Trans. Software Eng., vol. 14, no. 6, pp. 868–874, June 1988.
[51] M.J. O'Donnell, Equational Logic as a Programming Language. MIT Press, 1985.
[52] D.L. Parnas, "On the Criteria to be Used in Decomposing Systems into Software Modules," Comm. ACM, Dec. 1972, pp. 1,053-1,058.
[53] C.V. Ramamoorthy, S.F. Ho, and W.T. Chen, “On the Automated Generation of Program Test Data,” IEEE Trans. Software Eng., vol. 2, pp. 293-300, 1976.
[54] S. Rapps and E.J. Weyuker, “Selecting Software Test Data Using Data Flow Information,” IEEE Trans. Software Eng., vol. 11, no. 4, pp. 367–375, Apr. 1985.
[55] S. Sankar,“Run-time consistency checking of algebraic specifications,”inProc. TAV4–The 4th Software Testing, Analysis and Verification Symp. ACM SIGSOFT, Oct. 1991, pp. 123–129.
[56] B. Stroustrup, The C Programming Language. Reading, Mass.: Addison-Wesley, 1986.
[57] D.M. Volpano and R.B. Kieburtz, “Software Templates,” Proc. Int'l Conf. Software Eng. '85, pp. 55-60, 1985.
[58] C. Wang and D.R. Musser, “Dynamic Verification of C++ Generic Algorithms,” IEEE Trans. Software Eng., vol. 23, no. 5, pp. 314-323, May 1997.
[59] Pamela Zave, "The Operational Versus the Conventional Approach to Software Development," Comm. ACM, vol. 27, p. 113, Feb. 1984.

Index Terms:
Self-checking code, object-oriented software testing, formal specification, rewriting.
Citation:
Sergio Antoy, Dick Hamlet, "Automatically Checking an Implementation against Its Formal Specification," IEEE Transactions on Software Engineering, vol. 26, no. 1, pp. 55-69, Jan. 2000, doi:10.1109/32.825766
Usage of this product signifies your acceptance of the Terms of Use.