源码逻辑评估

Question

我得到了一段代码（例如，一个名为 bubbleSort() 的函数，用 Java 编写）。我，或者更确切地说，我的程序如何判断给定的源代码是否以正确的方式实现了特定的排序算法（例如，使用冒泡法）？

我可以通过分析函数签名强制用户提供合法函数：确保参数和 return 值是一个整数数组。但我不知道如何确定算法逻辑是否以正确的方式完成。输入代码可以正确地对值进行排序，但不是在前面提到的冒泡方法中。我的程序如何识别？我确实意识到会涉及很多代码解析，但也许还有其他我应该知道的事情。

希望我说得比较清楚。

如果有人能指出正确的方向或就如何解决此类问题提出建议，我将不胜感激。也许有经过测试的方法可以简化程序逻辑的评估。

Answer 1

一般来说，由于停机问题，您不能这样做。您甚至无法决定函数是否会停止 ("return")。

作为一个实际问题，还有更多的希望。如果你正在寻找冒泡排序，你可以决定它有几个部分：

具有部分顺序的待排序数据类型 S，
具有单个实例变量 A 的容器数据类型 C ("the array")
保存待排序数据
一个key类型K("array index")用于访问有偏序的容器这样 container[K] 的类型是 S
使用密钥 A 和密钥 B 比较容器的两个成员使得 A < B 根据键偏序，确定如果容器[B]>容器A
container[A]、container[B] 和 S 类型的某个变量 T 的交换操作，有条件地依赖于比较
环绕容器的循环，根据 K

您可以构建一些代码，在您的源代码中找到这些证据中的每一个，如果您找到所有这些证据，则声称您有冒泡排序的证据。

要具体执行此操作，您需要标准的程序分析机制：

解析源码构建抽象语法树
构建符号表 (ST) 以了解每个标识符的类型
构造一个控制流图 (CFG)，以便您检查各种可识别的位是否以适当的顺序出现
构造一个数据流图 (DFG)，以便您可以确定在算法的一部分中识别的值正确地流向另一部分

[刚开始需要很多机器]

从这里开始，您可以编写临时代码程序代码来爬过 AST、ST、CFG、DFG 到 "recognize" 每个单独的部分。这可能会非常混乱，因为每个识别器都会检查这些结构以获取其位的证据。但是，你可以做到。

这已经够乱了，也够有趣了，所以有一些工具可以做很多这样的事情。

我们的 DMS 软件再造工具包就是其中之一。 DMS 已经包含了对多种语言进行标准程序分析的所有机制。 DMS 还有一种数据流模式匹配语言，灵感来自 Rich and Water's 1980's "Programmer's Apprentice" ideas。

使用 DMS，您可以粗略地表达这个特定问题（未经测试）：

 dataflow pattern domain C;

 dataflow pattern swap(in out v1:S, in out v2:S, T:S):statements =
    " \T = \v1;
      \v1 = \v2;
      \v2 = \T;";

 dataflow pattern conditional_swap(in out v1:S, in out v2:S,T:S):statements=
     " if (\v1 > \v2)
          \swap(\v1,\v2,\T);"

 dataflow pattern container_access(inout container C, in key: K):expression
     = " \container.body[\K] ";

 dataflow pattern size(in container:C, out: integer):expression
     = " \container . size "

 dataflow pattern bubble_sort(in out container:C, k1: K, k2: K):function
     "  \k1 = \smallestK\(\);
        while (\k1<\size\(container\)) {
           \k2 = \next\(k1);
           while (\k2 <= \size\(container\) {
               \conditionalswap\(\container_access\(\container\,\k1\),
                                 \container_access\(\container\,\k2\)  \)
           }
       }
    ";

在每个模式中，您可以编写相当于所选编程语言 ("pattern domain") 的具体语法，引用模式签名行中命名的数据流。一个子模式可以在另一个内部被提及；必须通过命名将数据流传入和传出子模式。与 "plain old C" 不同，您必须显式传递容器，而不是通过隐式引用；那是因为我们对从模式中的一处流向另一处的实际值感兴趣。（仅仅因为代码中的两个地方使用相同的变量，并不意味着它们看到相同的值）。

给出这些定义，并询问 "match bubble_sort"，DMS 将访问 DFG（绑定到 CFG/AST/ST）以尝试匹配模式；在匹配的地方，它将模式变量绑定到 DFG 条目。如果找不到所有匹配项，则匹配失败。

为了完成匹配，上面的每个模式本质上都被转换成它自己的 DFG，然后使用所谓的子图同构测试将每个模式与代码的 DFG 进行匹配。为模式构建 DFG 需要 lot 机器：解析、名称解析、控制和数据流分析，应用于原始语言的代码片段，与各种模式元转义混合.子图同构对编码来说是 "sort of easy"，但对运行来说可能非常昂贵。拯救 DMS 模式匹配器的是大多数模式都有很多很多约束[技术点：并且它们没有结]并且每次尝试的匹配往往很快就会失败，或者完全成功。

未显示，但通过分别定义各种位，可以提供替代实现，从而能够识别变体。

我们已经使用它来实现非常完整的工厂控制模型提取工具，从陶氏化学的真实工厂控制器中使用他们特有的 Dowtran 语言（意味着构建解析器等，如上文所述，用于 Dowtran）。我们有这个原型的 C 版本；数据流分析更难。

源码逻辑评估

Source code logic evaluation

parsing

token

grammar

abstract-syntax-tree