Статический анализ нескольких операторов if (условий)

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 никогда не будет вызван.

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

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

UPDATE:

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

Answer 1

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

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

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

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

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

Answer 2

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

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

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

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

Answer 3

В общем случае это, как пишет @Michael Donohue, проблема 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

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