|symbolic interpretation email@example.com (Lorenzo Bettini) (2001-01-11)|
|Re: symbolic interpretation firstname.lastname@example.org.OZ.AU (2001-01-18)|
|Re: symbolic interpretation email@example.com (Ira D. Baxter) (2001-01-18)|
|Re: symbolic interpretation firstname.lastname@example.org (Steven Carroll) (2001-01-18)|
|Re: symbolic interpretation email@example.com (Basile STARYNKEVITCH) (2001-01-19)|
|Re: symbolic interpretation firstname.lastname@example.org.OZ.AU (2001-01-26)|
|From:||email@example.com.OZ.AU (Fergus Henderson)|
|Date:||26 Jan 2001 16:54:33 -0500|
|Organization:||Computer Science, University of Melbourne|
|References:||01-01-072 01-01-079 01-01-107|
|Posted-Date:||26 Jan 2001 16:54:33 EST|
Basile STARYNKEVITCH <firstname.lastname@example.org> writes:
>>>>>> "Fergus" == Fergus Henderson <email@example.com.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,
>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 <firstname.lastname@example.org> | "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
Search the comp.compilers archives again.