G. A. Venkatesh
ABSTRACT
Abstract interpretation introduced the notion of formal specification of program analyses. Denotational frameworks are convenient for reasoning about such specifications. However, implementation considerations make denotational specifications complex and hard to develop. We present a framework that facilitates the construction and understanding of denotational specifications for program analysis techniques. The framework is exemplified by specifications for program analysis techniques from the literature and from our own research. This approach allows program analysis techniques to be incorporated into automatically generated program synthesizers by including their specifications with the language definition.
- 1.A. W. Appel, "Semantics-Directed Code Generation," pp. 315-324 in Proc. 12th ACM Syrup. on Principles of Programming Languages, (January 1985). Google Scholar
Digital Library
- 2.P. Cousot and R. Cousot, "Abstract interpretation: A Unified Lattice Model for Static Amlysi~ of Programs by Construction or Approximation of Fixpoints," pp. 238-252 in Proc. 4th ACM $yrnp. on Principles of Programming Languages, (January 1977). Google ScholarDigital Library
- 3.Allan Demers, Thomas Reps, and Tim Teitelbaum, "Incremental evaluation for attribute grammars with application to syntax-directed editors.," pp. 105-116 in Proc. 8th ACM Symp. on Principles of Programming Languages, (1981). Google ScholarDigital Library
- 4.P. Hudak, "A semantic model of reference counting and its abstraction," pp. 45-62 in Abstract Interpretation of Declarative Languages, ed. S. Abramslcy, C. Hankin,Ellia Horwood, West Sussex (1987).Google Scholar
- 5.P. Hudak and J. Young, "A Collecting Interpretation of ExFressions (Without Powerdomains)," pp. 107-118 in Proc. 15th ACM Syrup. on Principles of Programming Languages, (January 1988). Google ScholarDigital Library
- 6.J. Hughes, "Analysing strictness by abstract interpretation of continuations," pp. 63-102 in Abstract Interpretation of Declarative Languages, exl. S. Abramsky, C. Hankin,Ellis Horwood, West Sussex (1987).Google Scholar
- 7.N.D. lones and S. S. Muchnik, "Complexity of flow analysis, inductive assertion synthesis and a language due to Dij3mtra," pp. 380-393 in Program flow analysis: Theory and applications, Prentice-Hall (1981 ).Google Scholar
- 8.N. D. Jones and A. Mycroft, "Data flow analysis of applicative programs using minimal function graphs.," pp. 296- 306 in Proc. 13th ACM Syrup. on Principles of Programming Languages, (January 1986). Google ScholarDigital Library
- 9.G. A. Kildall, "A Unified Approach to Global Program Optimization," ACM Syrup. on Princ~oles of Programming Languages, pp. 194-206 (1973). Google ScholarDigital Library
- 10.F. Nielson, "A denotational framework for data flow analysis," Acta Informatica 18 pp. 265-287 (1982).Google ScholarDigital Library
- 11.A. Pal, "Generating Execution Facilities for Integrated Programming Environments," Tech. Report 676, University of Wisconsin-Madison (1986). Ph.D. thesis Google ScholarDigital Library
- 12.U.F. Pleban, "Compiler Prototyping Ushlg Formal Semantics,'' pp. 94-105 in Proceedings of the SIGPLAN' 84 Symposium on Compiler Construction, , Montreal, Canada (June 1984). Google ScholarDigital Library
- 13.W.W. Pugh, "Incremental computation and the incremental evaluation of function programs," Tech. Report 88-936, Comell University (1988). Ph.D. thesis Google ScholarDigital Library
- 14.T. Reps and T. Teitelbaum, The Synthesizer Generator Reference Manual, Springer-Verlag, New York (Third Edition, 1988). Google ScholarDigital Library
- 15.R. Sethi, "Control Flow Aspects of Semantics-Directed Compiling," ACM Transactions on Programming languages and Systems $(4X1983). Google ScholarDigital Library
- 16.O.A. Venkatesh and C. N. Fischer, "A framework for denotational specification of program analysis techniques," Tech. Report in preparation, University of Wisconsin- Madison (1989).Google Scholar
- 17.G.A. Venkatesh and C. N. Fischer, "Construction of program analysis techniques for use in program development environments," Tech. Report #811, University of Wisconsin-Madison (1989).Google Scholar
- 18.M.N. Wegman and F. K. Zadeck, "Constant propagation with conditional branches," Tech. Report #CS-88-02, Brown University (1988). Google ScholarDigital Library
Index Terms
- A framework for construction and evaluation of high-level specifications for program analysis techniques
Recommendations
A framework for construction and evaluation of high-level specifications for program analysis techniques
Proceedings of the SIGPLAN '89 symposium on Interpreters and interpretive techniquesAbstract interpretation introduced the notion of formal specification of program analyses. Denotational frameworks are convenient for reasoning about such specifications. However, implementation considerations make denotational specifications complex ...
Informality in Program Specifications
This paper is concerned with the need for computer-based tools which help human designers formulate formal process-oriented specifications. It first determines some attributes of a suitable process-oriented specification language, then examines the ...
Comments