Nevin Heintze
Skip Abstract Section
Abstract
Reasoning about program variables as sets of “values” leads to a simple, accurate and intuitively appealing notion of program approximation. This paper presents approach for the compile-time analysis of ML programs. To develop the core ideas of the analysis, we consider a simple untyped call-by-value functional language. Starting with an operational semantics for the language, we develop an approximate “set-based” operational semantics, which formalizes the intuition of treating program variables as sets. The key result of the paper is an O(n3) algorithm for computing the set based approximation of a program. We then extend this analysis in a natural way to deal with arrays, arithmetic, exceptions and continuations. We briefly describe our experience with an implementation of this analysis for ML programs.
- 1 A. Aiken and E. Wimmers, "Solving Systems of Set Constraints", Proc. 7tn IEEE Syrup. on Logic in Com. purer Science, Santa Cruz, pp. 329-340, June 1992.Google Scholar
Cross Ref
- 2 A. Aiken and E. Wimmers, "Type Inclusion and Type Inference", Proc. 6*n A CM Con/. on Functional Programming and Computer Architecture, Copenhagen, pp. 31-41, June 1993. Google ScholarDigital Library
- 3 A. Aiken, E. Wimmers and T.K. Lakshman, "Soft Typing with Conditional Types" Proc. 21*h ACM Syrup. on Principles o/Programming Languages, Portland, OR, pp. 163-173, January 1994. Google ScholarDigital Library
- 4 A. Appel, "Compiling with Continuations", Cambridge University Press, 1992. Google ScholarDigital Library
- 5 L. Bachmair, H. Ganzinger and U. Waldmann, "Set Constraints are the Monadic Class", Technical Report MPI-I-92-240, Max-Planck-institute for Computer Science, December 1992.Google Scholar
- 6 E. Biagioni, R. Harper, P. Lee, and B. Milnes, "Signatures for a network protocol stack: A systems application of Standard ML", Proc. 199~i ACM Conf. on Lisp and Functional Programming, Orlando, Florida, June 1994, to appear. Google ScholarDigital Library
- 7 R. Cartwright and M. Fagan, "Soft Typing", Proc. 1991 A CM Conj. on Programming Language Design and Implementation, Toronto, pp. 278-292, June 1991. Google ScholarDigital Library
- 8 C. Consel and O. Danvy, "Tutorial Notes on Partial Evaluation", Proc. 20tn ACM Syrup. on Principle8 of Programming Languages, Charleston, pp. 493-501, January 1993. Google ScholarDigital Library
- 9 P. Cousot and R. Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints", Proc. 4*h A CM Syrup. on Principles of Programming Languages, Los Angeles, pp. 238-252, January 1977. Google ScholarDigital Library
- 10 N. Heintze, "Set-Based Program Analysis", Ph.D. thesis, School of Computer Science, Carnegie Mellon University, October 1992. Google ScholarDigital Library
- 11 N. Heintze, "Set-Based Program Analysis and Arithmetic'', Technical Report, School of Computer Science, Carnegie Mellon University, December 1993. Google ScholarDigital Library
- 12 N. Heintze and J. Jaffar, "A Finite Presentation Theorem for Approximating Logic Programs", Proc. 17tn A CM Syrup. on Principles o} Programming Languages, San Francisco, pp. 197-209, January 1990. (A full version of this paper appears as IBM Technical Report RC 16089 (~ 71415), 66 pp., August 1990.) Google ScholarDigital Library
- 13 N. Heintze and J. Jaffar, "A Decision Procedure for a Class of Herbrand Set Constraints", Proc. 5th IEEE Syrup. on Logsc, n Computer Science, Philadelphia, pp. 42-51, June 1990. (A full version of this paper appears as Carnegie Mellon University Technical Report CMU-CS-91-110, 42 pp., February 1991.)Google Scholar
- 14 N. Heintze and J. Jaffar, "An Engine for Logic Program Analysis", Proc. 7th IEEE Syrup. on Logic in Computer Science, Santa Cruz, pp. 318-328, June 1992.Google ScholarCross Ref
- 15 F. Henglein, "Efficient Type Inference for Higher- Order Binding-Time Analysis", Proceedings 5*n A CM- FPCA, Cambridge MA, LNCS 523, pp. 448-472, August 1991. Google ScholarDigital Library
- 16 T. Jensen and T. Mogensen, "A Backwards Analysis for Compile-Time Garbage Collection", Proc. 3ra European Syrup. on Programming, Copenhagen, LNCS 432, pp. 227-239, May 1990. Google ScholarDigital Library
- 17 N. Jones, "Flow Analysis of Lazy Higher-Order Functional Programs", in Abstract Interpretation of Declarative Languages, S. Abramsky and C. Hankln (Eds.), Ellis Horwood, 1987.Google Scholar
- 18 N. Jones, C. Gomard and P. Sestoft, "Partial Evaluation and Automatic Program Generation", "Prentice- Hall International", 1993. Google ScholarDigital Library
- 19 N. Jones and S. Muchnick, "Flow Analysis and Optimization of LISP-like Structures", Proc. 6th A CM Syrup. on Principles of Programming Languages, San Antonio, pp. 244-256, January 1979. Google ScholarDigital Library
- 20 N. Jones and S. Muchnick, "Complexity of Flow Analysis, Inductive Assertion Synthesis, and a Language due to Dijkstra", Proc. 21~t IEEE-FOCS, Syracuse, pp. 185-190, October 1980. (Also in, Program Flow Analttsis: Theory and Applications, N. Jones and S. Muchnick (Eds.), Prentice-Hall, 1981.) Google ScholarDigital Library
- 21 K. Malmkjeer, N. Heintze and O. Danvy, "ML Partial Evaluation using Set-Based Analysis", submitted for publication.Google Scholar
- 22 R. Milner, M. Torte and R. Harper, "The Definition of Standard ML', MIT Press, 1990. Google ScholarDigital Library
- 23 T. Mogensen, ~Separating Binding Times in Language Specifications", Proc. Functional Programming and Computer Architecture, London, ACM, pp. 12-25, September 1989. Google ScholarDigital Library
- 24 F. Nielson and H. Nielson, "Two-Level Functional Languages", Cambridge University Press, Vol 34, Cambridge Tracts in Theoretical Computer Science, 1992. Google ScholarDigital Library
- 25 O. Shivers, "Control Flow AnMysis in Scheme", Proc. 1988 A CM Conf. on Programming Language Design and Implementation, Atlanta, pp. 164-174, June 1988. Google ScholarDigital Library
- 26 J. Palsberg, Private Communication, November 1993.Google Scholar
- 27 J. Palsberg and M. Schwartzbach, "Safety Analysis versus Type Inference for Partial Types" Informstion Processing Letters, Vol 43, pp. 175-180, North- Holland, September 1992. Google ScholarDigital Library
- 28 J. Palsberg and M. Schwartzbach, "Object-Oriented Type Systems", John Wiley & Sons, to appear, 1993. Google ScholarDigital Library
- 29 J. Reynolds, "Automatic Computation of Data Set Definitions", In/ormation Processing 68, pp. 456-461, North-Holland, 1969.Google Scholar
- 30 A. Wright and R. Cartwright, "A Practical Soft Type System for Scheme", Proc. 199j A CM Conf. on Lisp and Functional Programming, Orlando, Florida, June 1994, to appear. Google ScholarDigital Library
Index Terms
- Set-based analysis of ML programs
Recommendations
Set-based analysis of ML programs
LFP '94: Proceedings of the 1994 ACM conference on LISP and functional programmingReasoning about program variables as sets of “values” leads to a simple, accurate and intuitively appealing notion of program approximation. This paper presents approach for the compile-time analysis of ML programs. To develop the core ideas of the ...
Specifying imperative ML-like programs using dynamic logic
FoVeOOS'10: Proceedings of the 2010 international conference on Formal verification of object-oriented softwareWe present a logical system suited for specification and verification of imperative ML programs. The specification language combines dynamic logic (DL), explicit state updates and second-order functional arithmetic. Its proof system is based on a ...
Comments