Детали компиляции и алгоритмы достижимости

Question

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

Я произвел разбор правила, выбрал (с помощью распознаваемого объединения) и упорядочил узлы в соответствии с потоком выполнения.Теперь я должен сделать своего рода статический анализ, чтобы сообщить пользователю, что для определенных условий некоторые узлы недоступны.Существует несколько точек входа в график, но только одна точка выхода.

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

let tryCondition cond =
if cond then
    if not cond then "Not reachable"
    else "Reachable"
else "bye"

или

let tryConditionTwo num =
match num with
| x as t when x > 0 -> match t with
                       | y when y < 0 -> "Not reachable"
                       | _ -> "Reachable"
| _ -> "bye"

Есть ли лучшее решение и не слишком много?Сложно реализовать в F # для решения этой проблемы?Или в компиляторе есть опция, которая позволяет мне получать информацию о недоступном коде?

Это пример графика, на котором я должен проверить достижимость различных ветвей.Блоки «IN» используются для загрузки столбцов из базы данных, а блоки «Выбрать» используются для выбора всех и только строк, соответствующих данному условию.Я должен статически проверить, что эти условия взаимно противоречивы.

Answer 1

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

Я не думаю, что компилятор F # делает что-либокомплексный анализ достижимости на данный момент.Если вы хотите реализовать эту проверку только для логических условий и целых чисел (как в ваших примерах), то вы можете проанализировать выражение F #, преобразовать его в некоторую логическую формулу и затем использовать SMT solver , чтобы проверить, есть лилюбые значения, для которых будет выполнено условие.

• Для анализа исходного кода вы можете использовать либо версию # 1011 * с открытым исходным кодом F # , либо использовать цитаты F #(если вы просто хотите запустить свой инструмент на явно помеченных выражениях).Использование последнего проще для запуска.

• Для получения дополнительной информации о решателях SMT вы можете проверить проект Z3 в Microsoft Research.Вы также можете реализовать простую версию такого инструмента самостоятельно - для просто логических условий (без чисел) вы можете взглянуть на SAT-алгоритмы решения .