This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Dynamic Verification of C++ Generic Algorithms
May 1997 (vol. 23 no. 5)
pp. 314-323

Abstract—Dynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification we also need to generate multiple program execution paths and use assertions (to handle while loops, for example), but we show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. We include an example of the formal verification of an STL generic algorithm.

[1] R.S. Boyer, B. Elspas, and K.N. Levitt, "SELECT—A Formal System for Testing and Debugging Programs by Symbolic Execution," Proc. Int'l Conf. Reliable Software, Apr. 1975.
[2] D. Evans, J. Guttag, J. Horning, and Y.M. Tan, "LCLint: A Tool for Using Specifications to Check Code," Proc. POPL Workshop Interface Definition Languages,Portland, Ore., Jan. 1994.
[3] P. Fritzson, M. Auguston, and N. Shahmehri, “Using Assertions in Declarative and Operational Models for Automated Debugging,” J. Systems Software, vol. 25, pp. 223–239, 1994.
[4] N.E. Fuchs, "Specifications Are (Preferably) Executable," Software Eng. J., vol. 7, Sept. 1992.
[5] J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J-P Jouannaud, Introducing OBJ. J.A. Goguen, D. Coleman, R. Gallimore, eds., "Application of Algebraic Specification Using OBJ," Cambridge Univ. Press, 1992.
[6] D. Gries, The Science of Programming.New York, Heidelberg, Berlin: Springer-Verlag, 1981.
[7] J. Guttag, J. Horning, S. Garland, K. Jones, A. Modet, and J. Wing, Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
[8] C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969.
[9] D. Kapur and D.R. Musser, "Tecton: A Framework for Specifying and Verifying Generic System Components," Technical Report 92-20, Dept. of Computer Science, Rensselaer Polytechnic Inst., July, 1992.
[10] D. Kapur, D.R. Musser, and A.A. Stepanov, "Tecton, A Language for Manipulating Generic Objects," Proc. Workshop Program Specification,Aarhus, Denmark, Aug. 1981, Lecture Notes in Computer Science 134, 1982.
[11] D. Kapur, D.R. Musser, and X. Nie, "An Overview of the Tecton Proof System," Theoretical Computer Science, vol. 133, pp. 307-339, 1994.
[12] J.C. King, A Program Verifier, PhD thesis, Carnegie Mellon Univ., 1969, p. 166.
[13] J.C. King, "A New Approach to Program Testing," Proc. Int'l Conf. Reliable Software, Apr. 1975.
[14] R.L. London and D.R. Musser, "The Application of a Symbolic Mathematical System to Program Verification," Proc. ACM Ann. Conf., Nov. 1974.
[15] D. Luckham, S. Sankar, and S. Takahashi, "Two-Dimensional Pinpointing: Debugging with Formal Specifications," IEEE Software, Jan. 1991.
[16] Luqi, H. Yang, and X. Zhang, "Constructing an Automated Testing Oracle: An Effort to Produce Reliable Software," Proc. Eighth Ann. Int'l Computer Software and Applications Conf., 1994.
[17] J.H. Morris and B. Wegbreit, "Program Verification by Subgoal Induction," Current Trends in Programming Methodology, R.T. Yeh, ed., vol. 2, ch. 8. Prentice Hall, 1977.
[18] D. Musser and A. Stepanov, The Ada Generic Library. Springer-Verlag, 1989.
[19] D.R. Musser and Changqing Wang, "A Basis for Formal Specification and Verification of Generic Algorithms in the C++ Standard Template Library," Technical Report 95-1, Dept. of Computer Science, Rensselaer Polytechnic Inst., Jan. 1995.
[20] W. Polak, "Program Verification Based on Denotational Semantics," Proc. Eighth Ann. ACM Symp. Principles of Programming Languages, 1981.
[21] D.J. Richardson, “TAOS: Testing with Analysis and Oracle Support,” Proc. Int'l. Symp. Software Testing and Analysis, 1994.
[22] D.S. Rosenblum, “A Practical Approach to Programming With Assertions,” IEEE Trans. Software Eng., vol. 21, no. 1, pp. 19–31, Jan. 1995.
[23] N. Shankar, S. Owre, and J.M. Rushby, "The PVS Specification Language," Computer Science Laboratory, SRI Int'l, Menlo Park, Calif., Mar. 1993.
[24] N. Shankar, S. Owre, and J.M. Rushby, The PVS Proof Checker: A Reference Manual, Computer Science Laboratory, SRI Int'l, Menlo Park, Calif, Mar. 1993
[25] S. Sankar and R. Hayes, "Specifying and Testing Software Components Using ADL," Technical Report SMLI TR-94-23, Sun Microsystems Lab, Inc., Apr. 1994.
[26] R.M. Stallman and R.H. Pesch, "Debugging with GDB," GDB User's Manual, Free Software Foundation, Inc., 1993.
[27] A. Stepanov and M. Lee, "The Standard Template Library," Technical Report, Hewlett-Packard Laboratories, Sept. 1994.
[28] A. Stepanov, M. Lee, and D.R. Musser, Hewlett-Packard Laboratories reference implementation of the Standard Template Library, source files available via anonymous ftp from butler.hpl.hp.com in /stl/sharfile.Z.
[29] C. Wang, "Integrating Tools and Methods For Rigorous Analysis of C++ Generic Library Components," PhD thesis, Dept of Computer Science, Rensselaer Polytechnic Institute, July, 1996.
[30] C. Wang and D.R. Musser, "Dynamic Verification of C++ Generic Components: A Practical Method and Its Support System," Proc. The First Workshop on Formal Methods in Software Practice,San Diego, Calif., Jan. 1996.
[31] J.M. Wing, “A Specifier's Introduction to Formal Methods,” IEEE Computer, vol. 23, pp. 8–24, Sept. 1990.
[32] J.M. Wing, "A Two-Tiered Approach to Specifying Programs," PhD thesis, Technical Report MIT/LCS/TR-299, Dept. of Electrical Eng. and Computer Science, MIT, May 1983.

Index Terms:
Specification, verification, generic algorithms, software libraries, C++, templates, Standard Template Library.
Citation:
Changqing Wang, David R. Musser, "Dynamic Verification of C++ Generic Algorithms," IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 314-323, May 1997, doi:10.1109/32.588523
Usage of this product signifies your acceptance of the Terms of Use.