Static inference of properties of applicative programs

ABSTRACT

An applicative program denotes a function mapping values from some domain to some range. Abstract interpretation of applicative programs involves using the standard denotation to describe an abstract function from a “simplified” domain to a “simplified” range, such that computation of the abstract function is effective and yields some information, such as type information, about the standard denotation. We develop a general framework for a restricted class of abstract interpretations that deal with non-strict functions defined on non-flat domains. As a consequence, we can develop inference schemes for a large and useful class of functional programs, including functions defined on streams. We describe several practical problems and solve them using abstract interpretation. These include inferring minor signatures and relevant clauses of functions, which have arisen out of our work on a strongly-typed applicative language.

REFERENCES

• 1: United States Department of Defense. Reference manual for the ADA programming language. United states Department of Defense, 1982.
• 2: M. Broy. Fixed point theory for communication and concurrency. Lectures at the International Summer school on Theoretical Foundations of Programming Methodology, July, 1981, pp.
• 3: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 4: Robert Cartwright , James Donahue, The semantics of lazy (and industrious) evaluation, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.253-264, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802157]
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: P. Cousot. Semantic Foundations of program analysis. In N.Jones and N.Muchnick, Ed., Program Flow Analysis: Theory and Applications, Prentice-Hall, 1981, pp. 303-342.
• 7: M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512773]
• 8: Peter Henderson, Functional Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1980
• 9: Christoph M. Hoffman , Michael J. O'Donnell, Programming with Equations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.1, p.83-112, Jan. 1982 [doi>10.1145/357153.357158]
• 10: P. Hudak. The aggregate update problem in functional programming systems. In preparation, Yale University, 1983
• 11: R.M. Keller, G.Lindstrom, and S.Patil. A loosely-coupled applicative multi-processing system. AFIPS, AFIPS, June, 1979, pp. 613-622.
• 12: R.M.Keller. Semantics and Applications of Function Graphs. Tech. Rept. UUCS-80-112, University of Utah, Computer Science Department, 1980.
• 13: Robert M. Keller, Divide and concer: Data structuring in applicative multiprocessing systems, Proceedings of the 1980 ACM conference on LISP and functional programming, p.196-202, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802806]
• 14: R.M.Keller. FEL Manual. University of Utah, 1983.
• 15: Richard B. Kieburtz, Precise typing of abstract data type specifications, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.109-116, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567079]
• 16: P. Mishra. Data Types in Applicative Languages: Abstraction and Inference. Ph. D. proposal, May 1983
• 17: P. Mishra, R.M. Keller. Optimized execution of a strongly typed applicative language. To appear, University of Utah, 1983
• 18: Alan Mycroft, The Theory and Practice of Transforming Call-by-need into Call-by-value, Proceedings of the Fourth 'Colloque International sur la Programmation' on International Symposium on Programming, p.269-281, April 22-24, 1980
• 19: A. Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. Th., University of Edinburgh, December 1981.
• 20: P. Panangaden, P.Mishra. General powerdomain constructions for abstract interpretation and indeterminacy. In preparation, University of Utah, 1983
• 21: G.D.Plotkin. "A Powerdomain Construction." SIAM J.Comput. 5, 3 (Sept. 1976), 452-480.
• 22: M.B.Smyth. "Power Domains." JCSS 16 (1978), 23-36.
• 23: William W. Wadge, An Extensional Treatment of Dataflow Deadlock, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.285-299, July 02-04, 1979