From: deutsch+@cs.cmu.edu (Alain Deutsch)
Newsgroups: comp.compilers
Subject: Re: Abstract Interpretation Query
Summary: AI applied to ADA; AI = DFA + proofs.
Keywords: functional, logic, bibliography, Ada
Date: 6 Sep 92 19:18:31 GMT
Reply-To: deutsch+@cs.cmu.edu (Alain Deutsch)
Followup-To: DEUTSCH@PROOF.ERGO.CS.CMU.EDU
Organization: School of Computer Science, Carnegie Mellon

>What I want to know is: has anybody applied it to everyday imperative
>languages in real life (i.e. to languages like Pascal, C, and
>analyses like type analysis, data flow analysis etc.)?  

Of course ! And for a long time.  For instance operational abstract
interpretation (AI) a la [Cousots77a] and in particular the interval
analysis for integer variables described in this paper and the alias
analysis described in [Cousots77b] have both successfuly been applied to
the automatic analysis of Ada programs (which certainly qualifies as a
real programming language), in order to safely eliminate array bound
checking and overflow checking.  The analysis has been implemented by
people from ALSYS and integrated in a real production compiler for Ada.
This was described in a paper written by E.  Morel and published by
Cambridge University Press (not sure) sometime between 82 and 86 in the
proceedings of a course on compilers that took place at INRIA, edited by
B.  Lorho which I do not have at hand right now.  For a survey on how to
apply these particular AI techniques and others to imperatives programming
languages, see [Cousots77c].

>If so, what were your experiences with Abstract Interpretation?  

My Phd subject was alias analysis for languages with structured data,
imperative operations, polymorphism and higher-order functions.  This
potentially covers a large spectrum of programming languages including ML
and Ada.

My experience has been very satisfactory so far, both theoretically and
practically as I end up with several algorithms, including one that
discovers a new kind of aliasing information not discovered by existing
algorithms.

What we should remember is what those who pioneered abstract
interpretation (Cousot & Cousot) had in mind, as formulated by F.
Nielson:

	AI = DFA + proofs

or in other words:

	ABSTRACT INTERPRETATION = DATA FLOW ANALYSIS + CORRECTNESS.

Correctness proofs set up a connection between the exact semantics
(operational a la Cousot or denotational a la Mycroft & Nielson) of the
programming language and the data flow analysis. Mathematically this
usually involves lattice theory, transfinite and fixpoint induction and
Galois connections.

I think it is important to have this in mind, and lots of people do not
seem to know that abstract interpretation is strongly connected to data
flow analysis, including researchers from both fields: abstract
abstraction and data flow analysis.

	Sincerely,

	Alain Deutsch.
----
Alain Deutsch -- School of Computer Science
Carnegie Mellon University, Pittsburgh, PA 15213-3891, USA.
Email: deutsch@cs.cmu.edu, Phone: (412) 268-6658, Fax: (412) 681-5739.

------------------------------------------------------------------------------
				REFERENCES:

@InProceedings{Cousots77a,
  author = 	"Cousot,P. and Cousot, R.",
  title = 	"Abstract Interpretation~: a unified lattice model for
		 static analysis of programs by construction of
		 approximation of fixpoints",
  booktitle = 	"Fourth Annual ACM Symp. on Principles of Programming Languages",
  year = 	"1977",
  pages = 	"238--252",
  address = 	"Los Angeles",
  month = 	jan
}

@InProceedings{Cousots77b,
  author = 	"Cousot,P. and Cousot,R.",
  title = 	"Static determination of dynamic properties of
		 recursive procedures",
  booktitle = 	"Working Conf. on Formal Description of
		 Programming Concepts",
  year = 	"1977",
  organization= "IFIP WG 2.2",
  publisher = 	"North-Holland",
  address = 	"St-Andrews,Canada",
  month = 	aug
}

@Article{Cousot77c,
  author = 	"Cousot,P. and Cousot,R.",
  title = 	"Static determination of dynamic properties of generalized
  	type unions",
  journal = 	"SIGPLAN Notices",
  year = 	1977,
  volume = 	12,
  number = 	3,
  pages = 	"77--94",
  month = 	mar
}

@Article{Nielson89,
  author = 	 "Nielson,F.",
  title = 	 "Two-level semantics and abstract interpretation",
  journal = 	 "Theoretical Computer Science",
  year = 	 1989,
  volume = 	 69,
  pages = 	 "117-242",
  month = 	 dec
}
-- 
Send compilers articles to compilers@iecc.cambridge.ma.us or
{ima | spdcc | world}!iecc!compilers.  Meta-mail to compilers-request.
Xref: sparky comp.compilers:1528 comp.theory:1886