|on definition of soundness and completeness email@example.com (Bin Xin) (2009-06-23)|
|Re: on definition of soundness and completeness firstname.lastname@example.org (Gene) (2009-07-05)|
|Re: on definition of soundness and completeness email@example.com (gopi) (2009-07-16)|
|From:||Bin Xin <firstname.lastname@example.org>|
|Date:||Tue, 23 Jun 2009 20:58:07 -0700 (PDT)|
|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
Completeness property (of F) can be claimed when: I \models P \implies
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?
Return to the
Search the comp.compilers archives again.