This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Extending Typestate Checking Using Conditional Liveness Analysis
May 1993 (vol. 19 no. 5)
pp. 478-485

The authors present a practical extension to typestate checking, which is capable of proving programs free of uninitialized variable errors even when these programs contain conditionally initialized variables where the initialization of a variable depends upon the equality of one or more tag variables to a constant. The user need not predeclare the relationship between a conditionally initialized variable and its tags, and this relationship may change from one point in the program to another. The technique generalizes liveness analysis to conditional liveness analysis. Like typestate checking, this technique incorporates a dataflow analysis algorithm in which each point in a program is labeled with a lattice point describing statically tracked information, including the initialization of variables. The labeling is then used to check for programming errors such as referencing a variable which may be uninitialized.

[1] A. V. Aho, R. Sethi, and J. D. Ullman,Compilers: Principles, Techniques, and Tools. Reading, MA: Addison-Wesley, 1986.
[2] P. Cousot and R. Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints,"Proc. Fourth Symp. Principles Programming Languages, ACM, New York, 1977, pp. 238-252.
[3] P. R. Eggert, "Detecting software errors before execution," Ph.D. dissertation, UCLA, 1980.
[4] L. D. Fosdick and L. J. Osterweil, "Data flow analysis in software reliability,"ACM Comput. Surveys, vol. 8, no. 3, pp. 306-330, Sept. 1976.
[5] L. H. Holley and B. K. Rosen, "Qualified data flow problems,"IEEE Trans. Software Eng., vol. SE-7, pp. 60-78, Jan. 1981.
[6] S. Horwitz, A. Demers, and T. Teitelbaum, "An efficient general iterative algorithm for data flow analysis,"Acta Informatica, vol. 24, pp. 679-694, 1987.
[7] N. D. Jones and S. S. Muchnik, "Complexity of flow analysis, inductive assertion synthesis and a language due to Dijkstra," inProgram Flow Analysis: Theory and Practice. Englewood Cliffs, NJ: Prentice-Hall, 1981, pp. 380-393.
[8] G. A. Kildall, "A unified approach to global program optimization," inProc. ACM Symp. on Principles of Program. Languages, 1973, pp. 194-206.
[9] T. J. Marlowe and B. G. Ryder, "Properties of dataflow frameworks,"Acta Informatica, vol. 28, pp. 121-163, 1990.
[10] K. Olender and L. Osterweil, "Cecil: A sequencing constraint language for automatic analysis generation,"IEEE Trans. Software Eng., vol. 16, pp. 268-280, Mar. 1990.
[11] R. Strom and S. Yemini, "Typestate: A programming language concept for enhancing software reliability,"IEEE Trans. Software Eng., vol. SE-12, pp. 157-171, Jan. 1986.
[12] R. E. Strom, "Mechanisms for compile-time enforcement of security," inProc. 10th ACM Symp. Principles of Programming Languages, ACM, Jan. 1983.
[13] R. E. Strom, D. F. Bacon, A. Goldberg, A. Lowry, D. Yellin, and S. A. Yemini,Hermes: A Language for Distributed Computing. Englewood Cliffs, NJ: Prentice-Hall, 1991.
[14] R. E. Strom and D. M. Yellin, "Computationally tractable semilattices for global data flow analysis," Tech. Rep. RC 14936, IBM T. J. Watson Res. Cen., Aug. 1989.
[15] R. E. Strom and S. A. Yemini, "NIL: An integrated language and system for distributed programming," inProc. SIGPLAN'83 Symp. Programming Language Issues in Software Syst., June 1983.
[16] M. Wegman and F. K. Zadeck, "Constant propagation with conditional branches,"ACM Trans. Programming Languages Syst., vol. 13, pp. 181-210, Apr. 1991.

Index Terms:
program verification; typestate checking; conditional liveness analysis; uninitialized variable errors; dataflow analysis algorithm; statically tracked information; programming errors; program verification
Citation:
R.E. Strom, D.M. Yellin, "Extending Typestate Checking Using Conditional Liveness Analysis," IEEE Transactions on Software Engineering, vol. 19, no. 5, pp. 478-485, May 1993, doi:10.1109/32.232013
Usage of this product signifies your acceptance of the Terms of Use.