This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Practical Approach to Programming With Assertions
January 1995 (vol. 21 no. 1)
pp. 19-31
Embedded assertions have been recognized as a potentially powerful tool for automatic runtime detection of software faults during debugging, testing, maintenance and even production versions of software systems. Yet despite the richness of the notations and the maturity of the techniques and tools that have been developed for programming with assertions, assertions are a development tool that has seen little widespread use in practice. The main reasons seem to be that (1) previous assertion processing tools did not integrate easily with existing programming environments, and (2) it is not well understood what kinds of assertions are most effective at detecting software faults. This paper describes experience using an assertion processing tool that was built to address the concerns of ease-of-use and effectiveness. The tool is called APP, an Annotation PreProcessor for C programs developed in UNIX-based development environments. APP has been used in the development of a variety of software systems over the past five years. Based on this experience, the paper presents a classification of the assertions that were most effective at detecting faults. While the assertions that are described guard against many common kinds of faults and errors, the very commonness of such faults demonstrates the need for an explicit, high-level, automatically checkable specification of required behavior. It is hoped that the classification presented in this paper will prove to be a useful first step in developing a method of programming with assertions.

[1] R. W. Floyd,“Assigning meanings to programs,”inProc. Symp. Appl. Math., vol. XIX, American Mathematical Society, Apr. 1967, pp. 19–32.
[2] S. Igarashi, R. L. London, and D. C. Luckham,“Automatic program verification I: A logical basis and its implementation,”Acta Informatica, vol. 4, pp. 145–182, 1975.
[3] D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis,“Stanford Pascal Verifier user manual,”Tech. Rep. 79-731, Dep. of Computer Science, Stanford University, Mar. 1979, Program Analysis and Verification Group Rep. 11.
[4] B. Meyer,“Applying design by contract,”IEEE Comput., vol. 25, pp. 40–51, Oct. 1992.
[5] L. G. Stucki and G. L. Foshee,“New assertion concepts for self-metric software validation,”inProc. Int. Conf. Reliable Software, ACM and IEEE Computer Society, Apr. 1975, pp. 59–71.
[6] B. W. Boehm, R. K. McClean, and D.B. Urfrig,“Some experience with automated aids to the design of large-scale reliable software,”inProc. Int. Conf. Reliable Software, ACM and IEEE Computer Society, Apr. 1975, pp. 105–113.
[7] S. S. Yau and R. C. Cheung,“Design of self-checking software,”inProc. Int. Conf. Reliable Software, ACM and IEEE Computer Society, Apr. 1975, pp. 450–457.
[8] B. W. Kernighan and D. M. Ritchie,The C Programming Language. Englewood Cliffs, NJ: Prentice-Hall, 1988, 2nd ed.
[9] B. Stroustrup,The C++ Programming Language. Reading MA: Addison-Wesley, 1991, 2nd ed.
[10] P. Gautron,“An assertion mechanism based on exceptions,”inProc. 4th C++ Tech. Conf., USENIX Association, Aug. 1992, pp. 245–262.
[11] M. P. Cline and D. Lea,“Using annotated C$++$,”inProc. C++ at Work, Sept. 1990.
[12] R. C. Holt and J. R. Cordy,“The Turing programming language,”Commun. ACM, vol. 31, no. 12, pp. 1410–1423, Dec. 1988.
[13] B. Meyer,Object-Oriented Software Construction. Englewood Cliffs, NJ: Prentice-Hall, 1988.
[14] D. E. Perry,“The Inscape environment,”inProc. 11th Int. Conf. Software Eng., IEEE Computer Society, May 1989, pp. 2–12.
[15] D. C. Luckham and F. W. von Henke,“An overview of Anna, a specification language for Ada,”IEEE Software, vol. 2, pp. 9–23, Mar. 1985.
[16] S. Sankar, D. S. Rosenblum, and R. B. Neff,“An implementation of Anna,”inAda in Use: Proc. Ada Int. Conf., May 1985, pp. 285–296, Cambridge Univ. Press.
[17] S. Sankar and D. S. Rosenblum,“The complete transformation methodology for sequential runtime checking of an Anna subset,”Tech. Rep. 86-301, Computer Systems Laboratory, Stanford Univ., June 1986, Program Analysis and Verification Group Report 30.
[18] S. Sankar,“Automatic Runtime Consistency Checking and Debugging of Formally Specified Programs,”Ph.D. thesis, Dep. of Computer Science, Stanford Univ., Aug. 1989 Tech. Rep. 89-1282.
[19] 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.
[20] D. S. Rosenblum, S. Sankar, and D. C. Luckham,“Concurrent runtime checking of Annotated Ada programs,”inProc. 6th Conf. Foundations of Software Tech. and Theoretical Comput. Sci. New York: Springer-Verlag (Lecture Notes in Computer Science No. 241), Dec. 1986, pp. 10–35
[21] S. Sankar and M. Mandal,“Concurrent runtime monitoring of formally specified programs,”IEEE Comput., vol. 26, pp. 32–41, Mar. 1993.
[22] D. C. Luckham,Programming with Specifications: An Introduction to Anna, a Language for Specifying Ada Programs. New York: Springer-Verlag, 1990.
[23] N. G. Leveson, S. S. Cha, J. C. Knight, and T. J. Shimeall,“The use of self checks and voting in software error detection: An empirical study,”IEEE Trans. Software Eng., vol. SE-16, pp. 432–443, Apr. 1990.
[24] D. E. Perry and W. M. Evangelist,“An empirical study of software interface faults,”inProc. Int. Symp. New Directions in Comput., IEEE Computer Society, Aug. 1985, pp. 32–38.
[25] ——,“An empirical study of software interface faults–an update,”inProc. 20th Ann. Hawaii Int. Conf. Syst. Sci., vol. II, Jan. 1987, pp. 113–126.
[26] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: Prentice-Hall, 1990, 2nd ed.
[27] J. M. Spivey,The Z Notation: A Reference Manual. Englewood Cliffs, NJ: Prentice-Hall, 1989.
[28] D. C. Luckham, F. W. von Henke, B. Krieg-Brückner, and O. Owe,Anna—A Language for Annotating Ada Programs. Lecture Notes in Computer Science No. 260. New York: Springer-Verlag, 1987.
[29] D. C. Luckham, S. Sankar, and S. Takahashi,“Two-dimensional pinpointing: Debugging with formal methods,”IEEE Software, vol. 8, pp. 74–84, Jan. 1991.
[30] S. I. Feldman,“Make—A program for maintaining computer programs,”Software—Practice and Experience, vol. 9, no. 3, pp. 255–265, Mar. 1979.
[31] G. S. Fowler,“A case for make,”Software—Practice and Experience, vol. 20, no. S1, pp. 35–46, June 1990.
[32] D. W. Flater, Y. Yesha, and E. K. Park,“Extensions to the C programming language for enhanced fault detection,”Software—Practice and Experience, vol. 23, no. 6, pp. 617–628, June 1993.
[33] T. M. Austin, S. E. Breach, and G. S. Sohi,“Efficient detection of all pointer and array access errors,”inProc. ACM SIGPLAN'94 Conf. Programm. Language Design and Implementation (PLDI), ACM SIGPLAN, June 1994, pp. 290–301, appears inSIGPLAN Notices29(6), June 1994.
[34] R. Hastings and B. Joyce,“Purify: Fast detection of memory leaks and access errors,”inProc. Winter 1992USENIX Conf., USENIX Association, Jan. 1992, pp. 125–136.
[35] D. S. Rosenblum and B. Krishnamurthy,“An event-based model of software configuration management,”inProc. 3rd Int. Workshop on Software Config. Management, P. H. Feiler, Ed., ACM SIGSOFT, June 1991, pp. 94–97.
[36] T. J. Ostrand and E. J. Weyuker,“Collecting and categorizing software error data in an industrial environment,”J. Syst. Software, vol. 4, pp. 289–300, 1984.
[37] A. Endres,“An analysis of errors and their causes in system programs,”IEEE Trans. Software Eng., vol. SE-1, pp. 140–149, June 1975.

Index Terms:
Anna, A<scp>PP</scp>, assertions, C, consistency checking, formal specifications, formal methods, programming environments, runtime checking, software faults.
Citation:
David S. Rosenblum, "A Practical Approach to Programming With Assertions," IEEE Transactions on Software Engineering, vol. 21, no. 1, pp. 19-31, Jan. 1995, doi:10.1109/32.341844
Usage of this product signifies your acceptance of the Terms of Use.