0

我是否应该对图的某些部分的可达性（称为规则）进行分析：如果验证了某个布尔条件，则可以到达一个节点。每个节点只知道它的前任，有不同类型的节点，并非所有节点都有要验证的条件。该规则被放置在一个文件中。

我做了规则的解析，我已经选择（通过使用有区别的联合）并按照执行流程对节点进行排序。现在，我应该进行一种静态分析，以告知用户，在特定条件下，某些节点是不可达的。图表有多个入口点，但只有一个出口点。

教授让我在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”块用于从数据库加载列，而“Select”块用于选择所有且仅满足给定条件的行。我应该静态地检查这些条件是否相互矛盾。

4

1 回答 1

3

没有简单的方法可以解决这个问题。如果您能够编写一个始终有效的静态分析工具，那么您也将解决停机问题，而这（可证明）是不可能的。

我认为 F# 编译器目前没有进行任何复杂的可达性分析。如果您只想对布尔条件和整数（如您的示例）实施此检查，那么您可以解析 F# 表达式，将其转换为一些逻辑公式，然后使用SMT 求解器检查是否有任何值符合条件将举行。

  • 要解析源代码，您可以使用开源 F#版本，也可以使用 F# 引用（如果您只想在显式标记的表达式上运行您的工具）。使用后者更容易开始。

  • 有关 SMT 求解器的更多信息，您可以查看 Microsoft Research 的Z3 项目。您也可以自己实现此类工具的简单版本 - 对于布尔条件（无数字），您可以查看SAT 求解算法。

于 2011-06-15T10:15:29.337 回答