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 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"... ;-)