Static analysis of multiple statements (conditions)
I have some 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 test two things (using static analysis):
- If all conditions
conditionA, conditionB, ..., conditionZ
are mutually exclusive (i.e. it is impossible for two or more conditions to be met at the same time). - All possible cases are covered, i.e. the "else throw" statement will never be called.
Could you please recommend a tool and / or a way that I could (easily) do this?
I would like more details than "use Prolog" or "Use Mathematica" ...; -)
UPDATE:
Suppose they conditionA, conditionB, ..., conditionZ
are (pure) functions and x, y, z are of "primitive" types.
a source to share
The 1. element you want to do is a stylistic issue. The program makes sense even if the conditions are not exceptional. Personally, as an author of static analysis tools, I think users get enough false alarms without trying to impose a style on them (and since another programmer would intentionally write overlapping conditions, that other programmer you are asking for would be false alarms). less, there are tools that can be customized: for one of them, you can write a rule that says that cases must be exclusive when this construct is encountered. And, as Jeffrey suggested, you can wrap your code in a context where you evaluate a boolean condition that is true if there is no overlap, and test that condition instead.
Element 2. is not a style issue: you want to know if an exception can be thrown.
The problem is complex in theory and practice, so tools usually give up at least correctness (never warning if there is a problem) or completeness (never warning about a non-problem). If the types of the variables were unbounded integers, the theory of computability would indicate that the parser cannot be both correct and complete and complete for all input programs. But enough with the theory. Some tools provide both correctness and completeness, and this does not mean that they are not useful either.
An example of the right tool is Frama-C value parsing: if it says that a statement (like the last case in the elseifs sequence) is unattainable, you know it is unattainable. It's not complete, so when he doesn't say the last statement is not available, you don't know.
An example of a completed Cute tool : It uses a so-called concolic to automatically generate test cases aimed at structural coverage (i.e. it will more or less heuristically try to generate tests that trigger the last case when all others have been accepted). Because it generates test cases (every single, defined input vector that the code actually runs on), it never warns that there are no problems. This is what it means to be complete. But it may not find a test case that will reach the last assertion, even if it is: it is incorrect.
a source to share
In general it is - as @Michael Donohue ponts out - an NP-hard issue.
But if you only have a reasonable number of conditions to check, you can simply write a program that checks them all.
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)
}
a source to share
Assuming your conditions are a boolean expression (and / or / not) over boolean-valued predicates X, Y, Z, your question is easily resolved with a symbolic boolean evaluator.
The question of whether they cover all cases is answered by accepting a contradiction with all conditions and asking if it is a tautology. Wang's algorithm does this just fine.
The question of whether they intersect is answered in pairs; for formulas a and b, symbolically construct a and b == false and reapply the Wang tautology test.
We used the DMS Software Reengineering Toolkit to perform similar boolean computations (partial evaluations) on conditional preprocessors in C. DMS provides the ability to parse the source code (important if you intend to do this across a large codebase and / or repeatedly when you modify your program over time), extract the chunks of the program, symbolically compose them, and then apply the rewrite rules (for carrying over from boolean simplifications or algorithms like Wang's).
a source to share