Re: symbolic interpretation

Basile STARYNKEVITCH <basile.starynkevitch@cea.fr> writes:


>>>>>> "Fergus" == Fergus Henderson <fjh@cs.mu.OZ.AU> writes:
>
> Fergus> I think "symbolic interpretation" is more commonly called
> Fergus> "abstract interpretation". (Or is there some difference
> Fergus> in these terms that I'm unaware of?)
>
>Abstract interpretation is a kind of static code analysis. In very
>primitive terms, it means executing the program with abstract values
>(for instance instead of executing a program on concrete numbers, you
>execute it on intervals, or other kind of lattices, etc...). The
>result is some crude approximation of the execution. Abstract
>interpretation is some kind of interpretation of the program with
>approximate set of values. (with some more technical tricks, widening,
>narrowing, etc...)
>
>Symbolic interpretation (or symbolic execution) is another kind of
>static code analysis. In naive terms, you execute the program with
>some properties (eg 1st order logic predicates) attached at most
>control points. Symbolic interpretation is more like automatic theorem
>proving related to programs.


I'm afraid I still don't see the difference. For abstract
interpretation, you also record properties, e.g. the abstract values
of variables, at control points of interest. Then you do a fixpoint
iteration to calculate the abstract values at those control points
(that's where those technical tricks like widening come into it --
they're needed to ensure termination of the fixpoint iteration).


Abstract interpretation is often done on functional or logic programs,
where all iteration is done via recursion, and so procedures
(functions / predicates) are often the only interesting control points.
So perhaps the difference is just that "abstract interpretation"
is what the functional/logic programming community calls it,
whereas "symbolic interpretation" is what the imperative programming
community calls it? ;-)


(I have a vague sense of deja vu about this discussion.
Has this issue come up before on comp.compilers?)
--
Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit
                                                                        | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
[The topic has come up, but I don't recall the details. -John]

Return to the comp.compilers page.
Search the comp.compilers archives again.