on definition of soundness and completeness

Bin Xin <bxin@acm.org>
Tue, 23 Jun 2009 20:58:07 -0700 (PDT)

          From comp.compilers

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)
| List of all articles for this month |

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?


Post a followup to this message

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