26 Jan 2001 16:54:33 -0500

Related articles |
---|

symbolic interpretation bettini@dsi.unifi.it (Lorenzo Bettini) (2001-01-11) |

Re: symbolic interpretation fjh@cs.mu.OZ.AU (2001-01-18) |

Re: symbolic interpretation idbaxter@semdesigns.com (Ira D. Baxter) (2001-01-18) |

Re: symbolic interpretation scarroll@csrd.uiuc.edu (Steven Carroll) (2001-01-18) |

Re: symbolic interpretation basile.starynkevitch@cea.fr (Basile STARYNKEVITCH) (2001-01-19) |

Re: symbolic interpretation fjh@cs.mu.OZ.AU (2001-01-26) |

From: | fjh@cs.mu.OZ.AU (Fergus Henderson) |

Newsgroups: | comp.compilers |

Date: | 26 Jan 2001 16:54:33 -0500 |

Organization: | Computer Science, University of Melbourne |

References: | 01-01-072 01-01-079 01-01-107 |

Keywords: | optimize |

Posted-Date: | 26 Jan 2001 16:54:33 EST |

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]

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.