Tue, 23 Jun 2009 20:58:07 -0700 (PDT)

Related articles |
---|

on definition of soundness and completeness bxin@acm.org (Bin Xin) (2009-06-23) |

Re: on definition of soundness and completeness gene.ressler@gmail.com (Gene) (2009-07-05) |

Re: on definition of soundness and completeness gopi.onthemove@gmail.com (gopi) (2009-07-16) |

From: | Bin Xin <bxin@acm.org> |

Newsgroups: | comp.compilers |

Date: | Tue, 23 Jun 2009 20:58:07 -0700 (PDT) |

Organization: | Compilers Central |

Keywords: | theory, question |

Posted-Date: | 25 Jun 2009 06:59:54 EDT |

In the presentation of various program analysis techniques, we often

read claims of "soundness" and "completeness" properties of those

techniques. I often find the definitions I expected for these two

concepts at odds with whatever is put down in the paper I am reading.

(I can give some fresh examples from latest conference like pldi).

So here is what I think these two concepts should be used, and I am

interested in finding out whether there is a standard way of using

these two terms or anything goes as long as they are defined in some

way each time.

My understanding is that: soundness and completeness are used to

describe the relationship between a formal system, F, and its

interpretations, I, in logic. For a given predicate, P, that we are

interested in, if it's True under interpretation I, then denote it as:

I \models P. If P can be proved or computed by the formal system F,

then denote it as: F \vdash P. Then,

Soundness property (of F) can be claimed when: F \vdash P \implies I

\models P.

and conversely,

Completeness property (of F) can be claimed when: I \models P \implies

F \vdash

In program analysis, the interpretation corresponds to the original

analysis problem we are trying to solve; the formal system is what is

actually being used/implemented to compute a solution (approximation,

often times) to the analysis problem.

Strangely, in papers that I feel those two terms are misused, some

used them in a reversed sense, i.e. calling what should be soundness

as completeness, and vice versa. Of course, I have found other cases

where the use of these two terms cannot be understand in the above

conceptual framework at all.

What is your take?

regards,

-b

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.