From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,bd26858f84fa9d43 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-09-24 07:05:03 PST From: Manuel Carro Newsgroups: comp.lang.ada Subject: Re: ANNOUNCE: New white paper available on www.sparkada.com Date: 24 Sep 2001 15:24:54 +0200 Organization: Computer Science Department, Technical U. of Madrid, Spain Message-ID: <7sn13ksoux.fsf@salmon.ls.fi.upm.es> References: NNTP-Posting-Host: salmon.ls.fi.upm.es Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: panoramix.fi.upm.es 1001337894 11149 138.100.10.4 (24 Sep 2001 13:24:54 GMT) X-Complaints-To: news@panoramix.fi.upm.es NNTP-Posting-Date: 24 Sep 2001 13:24:54 GMT User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/20.7 Path: archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!logbridge.uoregon.edu!news.rediris.es!news-2.rediris.es!138.100.251.9.MISMATCH!news.upm.es!panoramix.fi.upm.es!not-for-mail Xref: archiver1.google.com comp.lang.ada:13287 Date: 2001-09-24T13:24:54+00:00 List-Id: > Do you have any links to description of what Abstract Interpretation > is - i.e. what is it based on? Basically it is a general means to analyze programs by mapping them into an abstract value space. As a simple example, all numbers can be mapped to either 0, positive, or negative, and the builtin operations be redefined accordingly, i.e., x * y = y * x, (0) * _ = (0) (+) * (+) = (+) (+) * (-) = (-) (-) * (-) = (-) .... The program is then run in the abstract domain, possibly several times, until the information concerning the program does not change. Then one might be able to infer that a variable is, e.g., always positive at some point. The good point is that having a finite abtract domain (with some mathematical properties) ensures termination of the analysis. The bad point is that, of course, information is lost both with respect to the actual program (I know that something is positive, but that does not help me to get rid of a "X > 3" test), and with respect to the abstract domain itself (i.e., I might end up with a variable which has "any value"). The abstract domain should be carefully chosen to reflect the properties one wants to study. The nice thing is that the analysis algorithm can be made (in principle) generic and be used with any abstract domain. There has been a lot of work in abstract interpretation in logic and declarative languages. -- || Manuel Carro -- DLSIIS || || e-mail: mcarro@fi.upm.es || || http://lml.ls.fi.upm.es/~boris || || http://clip.dia.fi.upm.es/Software/Ciao || || Phone: +34 91 336-7455 FAX: +34 91 336-7412 ||