home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #20 / NN_1992_20.iso / spool / comp / compiler / 1526 < prev    next >
Encoding:
Internet Message Format  |  1992-09-08  |  4.7 KB
  1. Path: sparky!uunet!cis.ohio-state.edu!rutgers!faatcrl!iecc!compilers-sender
  2. From: deutsch+@cs.cmu.edu (Alain Deutsch)
  3. Newsgroups: comp.compilers
  4. Subject: Re: Abstract Interpretation Query
  5. Summary: AI applied to ADA; AI = DFA + proofs.
  6. Keywords: functional, logic, bibliography, Ada
  7. Message-ID: <92-09-045@comp.compilers>
  8. Date: 6 Sep 92 19:18:31 GMT
  9. References: <92-09-038@comp.compilers>
  10. Sender: compilers-sender@iecc.cambridge.ma.us
  11. Reply-To: deutsch+@cs.cmu.edu (Alain Deutsch)
  12. Followup-To: DEUTSCH@PROOF.ERGO.CS.CMU.EDU
  13. Organization: School of Computer Science, Carnegie Mellon
  14. Lines: 112
  15. Approved: compilers@iecc.cambridge.ma.us
  16.  
  17. >What I want to know is: has anybody applied it to everyday imperative
  18. >languages in real life (i.e. to languages like Pascal, C, and
  19. >analyses like type analysis, data flow analysis etc.)?  
  20.  
  21. Of course ! And for a long time.  For instance operational abstract
  22. interpretation (AI) a la [Cousots77a] and in particular the interval
  23. analysis for integer variables described in this paper and the alias
  24. analysis described in [Cousots77b] have both successfuly been applied to
  25. the automatic analysis of Ada programs (which certainly qualifies as a
  26. real programming language), in order to safely eliminate array bound
  27. checking and overflow checking.  The analysis has been implemented by
  28. people from ALSYS and integrated in a real production compiler for Ada.
  29. This was described in a paper written by E.  Morel and published by
  30. Cambridge University Press (not sure) sometime between 82 and 86 in the
  31. proceedings of a course on compilers that took place at INRIA, edited by
  32. B.  Lorho which I do not have at hand right now.  For a survey on how to
  33. apply these particular AI techniques and others to imperatives programming
  34. languages, see [Cousots77c].
  35.  
  36. >If so, what were your experiences with Abstract Interpretation?  
  37.  
  38. My Phd subject was alias analysis for languages with structured data,
  39. imperative operations, polymorphism and higher-order functions.  This
  40. potentially covers a large spectrum of programming languages including ML
  41. and Ada.
  42.  
  43. My experience has been very satisfactory so far, both theoretically and
  44. practically as I end up with several algorithms, including one that
  45. discovers a new kind of aliasing information not discovered by existing
  46. algorithms.
  47.  
  48. What we should remember is what those who pioneered abstract
  49. interpretation (Cousot & Cousot) had in mind, as formulated by F.
  50. Nielson:
  51.  
  52.     AI = DFA + proofs
  53.  
  54. or in other words:
  55.  
  56.     ABSTRACT INTERPRETATION = DATA FLOW ANALYSIS + CORRECTNESS.
  57.  
  58. Correctness proofs set up a connection between the exact semantics
  59. (operational a la Cousot or denotational a la Mycroft & Nielson) of the
  60. programming language and the data flow analysis. Mathematically this
  61. usually involves lattice theory, transfinite and fixpoint induction and
  62. Galois connections.
  63.  
  64. I think it is important to have this in mind, and lots of people do not
  65. seem to know that abstract interpretation is strongly connected to data
  66. flow analysis, including researchers from both fields: abstract
  67. abstraction and data flow analysis.
  68.  
  69.     Sincerely,
  70.  
  71.     Alain Deutsch.
  72. ----
  73. Alain Deutsch -- School of Computer Science
  74. Carnegie Mellon University, Pittsburgh, PA 15213-3891, USA.
  75. Email: deutsch@cs.cmu.edu, Phone: (412) 268-6658, Fax: (412) 681-5739.
  76.  
  77. ------------------------------------------------------------------------------
  78.                 REFERENCES:
  79.  
  80. @InProceedings{Cousots77a,
  81.   author =     "Cousot,P. and Cousot, R.",
  82.   title =     "Abstract Interpretation~: a unified lattice model for
  83.          static analysis of programs by construction of
  84.          approximation of fixpoints",
  85.   booktitle =     "Fourth Annual ACM Symp. on Principles of Programming Languages",
  86.   year =     "1977",
  87.   pages =     "238--252",
  88.   address =     "Los Angeles",
  89.   month =     jan
  90. }
  91.  
  92. @InProceedings{Cousots77b,
  93.   author =     "Cousot,P. and Cousot,R.",
  94.   title =     "Static determination of dynamic properties of
  95.          recursive procedures",
  96.   booktitle =     "Working Conf. on Formal Description of
  97.          Programming Concepts",
  98.   year =     "1977",
  99.   organization= "IFIP WG 2.2",
  100.   publisher =     "North-Holland",
  101.   address =     "St-Andrews,Canada",
  102.   month =     aug
  103. }
  104.  
  105. @Article{Cousot77c,
  106.   author =     "Cousot,P. and Cousot,R.",
  107.   title =     "Static determination of dynamic properties of generalized
  108.       type unions",
  109.   journal =     "SIGPLAN Notices",
  110.   year =     1977,
  111.   volume =     12,
  112.   number =     3,
  113.   pages =     "77--94",
  114.   month =     mar
  115. }
  116.  
  117. @Article{Nielson89,
  118.   author =      "Nielson,F.",
  119.   title =      "Two-level semantics and abstract interpretation",
  120.   journal =      "Theoretical Computer Science",
  121.   year =      1989,
  122.   volume =      69,
  123.   pages =      "117-242",
  124.   month =      dec
  125. }
  126. -- 
  127. Send compilers articles to compilers@iecc.cambridge.ma.us or
  128. {ima | spdcc | world}!iecc!compilers.  Meta-mail to compilers-request.
  129.