This Article 
 Bibliographic References 
 Add to: 
SPARE: A Development Environment for Program Analysis Algorithms
April 1992 (vol. 18 no. 4)
pp. 304-318

A tool that bridges the gap between the theory and practice of program analysis specifications is described. The tool supports a high-level specification language that enables clear and concise expression of analysis algorithms. The denotational nature of the specifications eases the derivation of formal proofs of correctness for the analysis algorithm. SPARE (structured program analysis refinement environment) is based on a hybrid approach that combines the positive aspects of both the operational and the semantics-driven approach. An extended denotational framework is used to provide specifications in a modular fashion. Several extensions to the traditional denotational specification language have been designed to allow analysis algorithms to be expressed in a clear and concise fashion. This extended framework eases the design of analysis algorithms as well as the derivation of correctness proofs. The tool provides automatic implementation for testing purposes.

[1] A. V. Aho, R. Sethi, and J. D. Ullman,Compilers: Principles, Techniques, and Tools. Reading, MA: Addison-Wesley, 1986.
[2] A. W. Appel, "Compile-time evaluation and code generation for semantics-directed compilers," Ph.D. thesis, Carnegie-Mellon Univ., 1985 (Tech. Rep. CMU-CS-85-147).
[3] 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.
[4] V. Donzeau-Gouge, "Denotational definition of properties of program computations," inProgram Flow Analysis: Theory and Applications. Englewood Cliffs, NJ: Prentice-Hall, 1981, pp. 343-379.
[5] C. N. Fischer and R. J. LeBlanc,Crafting a Compiler. Menlo Park, CA: Benjamin-Cummings, 1988.
[6] S. Horwitz, J. Prins, and T. Reps, "Integrating non-interfering versions of programs," inProc. Fifteenth ACM Symp. Principles of Programming Languages, ACM, New York, 1988, pp. 133-145.
[7] P. Hudak, "A semantic model of reference counting and its abstraction," inAbstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin, Eds. West Sussex, UK: Ellis Horwood, 1987, pp. 45-62.
[8] J. Hughes, "Analyzing strictness by abstract interpretation of continuations," inAbstract Interpretation of Declarative Languages, S. Abramsky and C. Hankin, Eds. West Sussex, UK: Ellis Horwood, 1987, pp. 63-102.
[9] N. D. Jones and A. Mycroft, "Data flow analysis of applicative programs using minimal function graphs," inProc. 13th ACM Symp. on Principles of Program. LanguagesJan. 1986, pp. 296-306.
[10] G. Kahn, "Natural semantics," inProc. Symp. on Theoretical Aspects of Comput. Sci., Feb. 1987.
[11] R. M. Keller and M. R. Sleep, "Applicative caching,"ACM TOPLAS, vol. 8, no. 1, pp. 88-106, Jan. 1986.
[12] G. A. Kildall, "A unified approach to global program optimization," inProc. ACM Symp. on Principles of Program. Languages, 1973, pp. 194-206.
[13] D. Michie, "'Memo' functions and machine learning,"Nature, vol. 218, pp. 19-22, 1968.
[14] J. Mostow and D. Cohen, "Automating program speedup by deciding what to cache," inProc. 9th Int. Joint Conf. on AI, 1985, vol. 1, pp. 165-172.
[15] F. Nielson, "A denotational framework for data flow analysis,"Acta Informatica, vol. 18, pp. 265-287, 1982.
[16] F. Nielson, "Abstract interpretation of denotational definitions," inProc. STACS'86. Berlin: Springer-Verlag, 1986, pp. 1-20.
[17] L. Paulson, "A semantics-directed compiler generator," inProc. 9th ACM Symp. on Principles of Program. Languages(Albuquerque, NM), 1982, pp. 224-233.
[18] U. F. Pleban, "Compiler prototyping using formal semantics," inProc. SIGPLAN'84 Symp. on Compiler Construction(Montreal, PQ, Can.), June 1984, pp. 94-105.
[19] W. W. Pugh, "Incremental computation and the incremental evaluation of function programs," Ph.D. thesis, Cornell Univ., 1988 (Tech. Rep. 88-936).
[20] J. Raoult and R. Sethi, "Properties of a notation for combining functions,"JACM, vol. 30, no. 3, pp. 595-611, 1983.
[21] T. Reps and T. Teitelbaum,The Synthesizer Generator Reference Manual, 3rd ed. New York: Springer-Verlag, 1988.
[22] D. A. Schmidt,Denotational Semantics--A Methodology for Language Development. Boston: Allyn and Bacon, 1986.
[23] J. E. Stoy,Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. Cambridge, MA: MIT Press, 1977.
[24] G. A. Venkatesh, "A framework for specification and implementation of program analysis algorithms," Ph.D. thesis, Univ. Wisconsin-Madison, Aug. 1989, (Tech. Rep. No. 875).
[25] G. A. Venkatesh, "A framework for construction and evaluation of high-level specifications for program analysis techniques," inProc. SIGPLAN'89 Conf. on Program. Language Design and Implementation, SIGPLAN Notices, vol. 24, no. 7, pp. 1-12, June 1989.
[26] G. A. Venkatesh and C. N. Fischer, "SPARE: reference manual," Univ. Wisconsin-Madison, Tech. Rep. No. 850, June 1989.
[27] G. A. Venkatesh and C. N. Fischer, "SPARE: formal semantics," Univ. Wisconsin-Madison, Tech. Rep. No. 873, Aug. 1989.
[28] M. N. Wegman and F. K. Zadeck, "Constant propagation with conditional branches," Brown Univ., Tech. Rep. No. CS-88-02, 1988.
[29] M. Weiser, "Program slicing,"IEEE Trans. Software Eng.vol. SE-10, pp. 352-357, July 1984.

Index Terms:
software tools; development environment; program analysis specifications; high-level specification language; SPARE; structured program analysis refinement environment; denotational specification; correctness proofs; testing; formal specification; program testing; programming environments; software tools; specification languages
G.A. Venkatesh, C.N. Fischer, "SPARE: A Development Environment for Program Analysis Algorithms," IEEE Transactions on Software Engineering, vol. 18, no. 4, pp. 304-318, April 1992, doi:10.1109/32.129219
Usage of this product signifies your acceptance of the Terms of Use.