Статический анализ нескольких, если заявления (условия)

Question

У меня есть код, подобный:

 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 

Я хотел бы проверить две вещи (с помощью статического анализа):

1. Если все условия conditionA, conditionB, ..., conditionZ взаимно (т. е. невозможно, чтобы одновременно выполнялись два или более условия).
2. Все возможные случаи покрыты, то есть инструкция «else throw» никогда не будет вызвана.

Не могли бы вы порекомендовать мне инструмент и/или способ, которым я мог бы (легко) это сделать?

Я был бы признателен за более подробную информацию, чем "использовать Пролог" или "использовать Mathematica" ... ;-)

UPDATE:

Пусть Предположим, что conditionA, conditionB, ..., conditionZ являются (чистые) функции и х, y, z имеют «примитивные» типы.

Answer 1

Пункт 1., который вы хотите сделать, является стилистической проблемой. Программа имеет смысл, даже если условия не являются исключительными. Лично, как автор инструментов статического анализа, я думаю, что пользователи получают достаточно ложных тревог, не пытаясь навязать им стиль (и поскольку другой программист намеренно писал бы перекрывающиеся условия, тому другому программисту, о чем вы просите, будет ложная тревога) , Тем не менее, есть инструменты, которые можно настроить: для одного из них вы можете написать правило, в котором говорится, что случаи должны быть эксклюзивными, когда эта конструкция встречается. И, как было предложено Джеффри, вы можете обернуть свой код в контексте, в котором вы вычисляете логическое условие, которое является истинным, если нет перекрытия, и вместо этого проверяйте это условие.

Пункт 2. не является проблемой стиля: вы хотите знать, может ли быть возбуждено исключение.

Проблема трудно в теории и на практике, поэтому инструменты обычно дают, по крайней мере один из правильности (никогда не предупредить, если есть проблема) или полноты (никогда не предупредит для не вопрос) , Если типы переменных были неограниченными целыми числами, теория вычислимости указала бы, что анализатор не может быть как правильным, так и полным и заканчиваться для всех входных программ. Но достаточно с теорией. Некоторые инструменты дают как правильность, так и полноту, и это не значит, что они тоже не полезны.

Пример правильного инструмента: Frama-C Анализ стоимости: если он говорит, что утверждение (например, последний случай в последовательности elseifs) недостижима, вы знаете, что оно недоступно. Это не полно, поэтому, когда он не говорит, что последнее утверждение недостижимо, вы не знаете.

Пример инструмента, который является полным является Cute: он использует так называемый concolic подхода для генерации тестовых случаев автоматически, с целью структурного покрытия (то есть, он будет более или менее эвристический пытается генерировать тесты, которые активизируют последние случай, когда все остальные были приняты). Поскольку он генерирует тестовые примеры (каждый отдельный, определенный входной вектор, на котором фактически выполняется код), он никогда не предупреждает об отсутствии проблем. Это то, что значит быть полным. Но он может не найти тестовый пример, который приведет к достижению последнего утверждения, даже если он есть: он неверен.

Answer 2

Это, по-видимому, изоморфно решению уравнения 3-sat, которое NP-твердое. К сожалению, вряд ли статический анализатор попытается охватить этот домен.

Answer 3

В общем случае это - как @Michael Donohue ponts out - проблема NP-hard.

Но если у вас есть достаточно разумного количества условий для проверки, вы можете просто написать программу, которая проверяет их все.

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) 
     } 

Answer 4

Предполагая, что ваши условия являются логическим выражением (и/или/нет) по булевозначным предикатам X, Y, Z, ваш вопрос легко решается с помощью символического логического механизма оценки.

На вопрос о том, охватывают ли они все случаи, отвечает, принимая дизъюнктин всех условий и спрашивая, является ли тавтология. Алгоритм Ван делает это просто отлично.

Вопрос о том, пересекаются ли они, отвечает попарно; для формул a и b, символически построить & b == false и снова применить тавтологический тест Ванга.

Мы использовали DMS Software Reengineering Toolkit для выполнения аналогичных вычислений логических значений (частичные оценки) по условным препроцессорам в C. DMS предоставляет возможность анализировать исходный код (важно, если вы намереваетесь сделать это через большую базу кода и/или несколько раз по мере изменения вашей программы с течением времени), извлекать фрагменты программы, символически составлять их, а затем применять правила перезаписи (для выполнения булевых упрощений или алгоритмов, таких как Wang's).