Static analysis of multiple if statements (conditions)

I have code similar to:

     if conditionA(x, y, z) then doA()
else if conditionB(x, y, z) then doB()
...
else if conditionZ(x, y, z) then doZ()
else throw ShouldNeverHappenException

I would like to validate two things (using static analysis):

1. If all conditions conditionA, conditionB, ..., conditionZ are mutually exclusive (i.e. it is not possible that two or more conditions are true in the same time).
2. All possible cases are covered, i.e. "else throw" statement will never be 开发者_JAVA技巧called.

Could you recommend me a tool and/or a way I could (easily) do this?

I would appreciate more detailed informations than "use Prolog" or "use Mathematica"... ;-)

UPDATE:

Let assume that conditionA, conditionB, ..., conditionZ are (pure) functions and x, y, z have "primitive" types.

---

The item 1. that you want to do is a stylistic issue. The program makes sense even if the conditions are not exclusive. Personally, as an author of static analysis tools, I think that users get enough false alarms without trying to force style on them (and since another programmer would write overlapping conditions on purpose, to that other programmer what you ask would be a false alarm). This said, there are tools that are configurable: for one of those, you could write a rule stating that the cases have to be exclusive when this construct is encountered. And as suggested by Jeffrey, you can wrap your code in a context in which you compute a boolean condition that is true iff there is no overlap, and check that condition instead.

The item 2. is not a style issue: you want to know if the exception can be raised.

The problem is difficult in theory and in practice, so tools usually give up at least one of correctness (never fail to warn if there is an issue) or completeness (never warn for a non-issue). If the types of the variables were unbounded integers, computability theory would state that an analyzer cannot be both correct and complete and terminate for all input programs. But enough with the theory. Some tools give up both correctness and completeness, and that doesn't mean they are not useful either.

An example of tool that is correct is Frama-C's value analysis: if it says that a statement (such as the last case in the sequence of elseifs) is unreachable, you know that it is unreachable. It is not complete, so when it doesn't say that the last statement is unreachable, you don't know.

An example of tool that is complete is Cute: it uses the so-called concolic approach to generate test cases automatically, aiming for structural coverage (that is, it will more or less heuristically try to generate tests that activate the last case once all the others have been taken). Because it generates test cases (each a single, definite input vector on which the code is actually executed), it never warns for a non-problem. This is what it means to be complete. But it may fail to find the test case that causes the last statement to be reached even though there is one: it is not correct.

---

This appears to be isomorphic to solving a 3-sat equation, which is NP-hard. It is unlikely a static analyzer would attempt to cover this domain, unfortunately.

---

In the general case this is—as @Michael Donohue ponts out—an NP-hard problem.

But if you have only a reasonable number of conditions to check, you could just write a program that checks all of them.

for (int x = lowestX; x <= highestX; x++)
    for (int y ...)
      for (int z ...)
      {
          int conditionsMet = 0;
          if conditionA(x, y, z) then conditionsMet++;
          if conditionB(x, y, z) then  conditionsMet++;
          ... 
          if conditionZ(x, y, z) then  conditionsMet++;
          if (conditionsMet != 1)
              PrintInBlinkingRed("Found an exception!", x, y, z)
      }

---

Assuming your conditions are boolean expression (and/or/not) over boolean-valued predicates X,Y,Z, your question is easily solved with a symbolic boolean evaluation engine.

The question about whether they cover all cases is answered by taking a disjunctiton of all the conditions and asking if is a tautology. Wang's algorithm does this just fine.

The question about whether they intersect is answered pairwise; for formulas a and b, symbolically construct a & b == false and apply Wang's tautology test again.

We've used the DMS Software Reengineering Toolkit to carry out similar boolean value computations (partial evaluations) over preprocessor conditionals in C. DMS provides the ability to parse source code (important if you intend to do this across a large code base and/or repeatedly as you modify your program over time), extract the program fragments, symbolically compose them, and then apply rewriting rules (to carry out boolean simplifications or algorithms such as Wang's).