on definition of soundness and completeness

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

Return to the comp.compilers page.
Search the comp.compilers archives again.