Set-based analysis of ML programs
- 1 July 1994
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Lisp Pointers
- Vol. VII (3) , 306-317
- https://doi.org/10.1145/182590.182495
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.Keywords
This publication has 14 references indexed in Scilit:
- An engine for logic program analysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Soft typing with conditional typesPublished by Association for Computing Machinery (ACM) ,1994
- A practical soft type system for SchemePublished by Association for Computing Machinery (ACM) ,1994
- Type inclusion constraints and type inferencePublished by Association for Computing Machinery (ACM) ,1993
- Safety analysis versus type inference for partial typesInformation Processing Letters, 1992
- Soft typingPublished by Association for Computing Machinery (ACM) ,1991
- Separating binding times in language specificationsPublished by Association for Computing Machinery (ACM) ,1989
- Control flow analysis in schemePublished by Association for Computing Machinery (ACM) ,1988
- Flow analysis and optimization of LISP-like structuresPublished by Association for Computing Machinery (ACM) ,1979
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977