源代码逻辑评估

我得到了一段代码（例如，用Java编写的名为bubbleSort（）的函数）。我怎样才能，或者更确切地说我的程序是否能够以给定的源代码以正确的方式实现特定的排序算法（例如使用泡沫方法）？源代码逻辑评估

我可以强制用户通过分析函数签名来给出一个合法的函数：确保参数和返回值是一个整数数组。但我不知道如何确定算法逻辑是以正确的方式完成的。输入代码可以正确排序值，但不能用前面提到的泡泡法。我的程序如何辨别？我意识到会涉及很多代码解析，但也许还有一些我应该知道的东西。

我希望我有点清楚。

如果有人能指出我正确的方向或就如何解决这样的问题提出建议，我将不胜感激。也许有些测试方法可以减轻程序逻辑的评估。

来源

2015-03-25 Linas

一般而言，由于停机问题，您无法执行此操作。你甚至不能决定函数是否会暂停（“返回”）。

作为一个实际问题，还有一点希望。如果你正在寻找一个冒泡排序，可以决定，它具有零件数量：

一个待排序的数据类型S采用偏序，
与单个实例变量的容器数据C型保持A（“阵列”）
所述待排序的数据
密钥K型（“数组索引”）用于访问具有部分顺序容器使得容器[K]是类型S
一个容器的两个成员的比较，使用密钥A和密钥B 使得A < B根据关键部分订单，确定了如果容器[B]>容器A
对容器[A]，容器[B]和S的某个变量T进行交换操作，即conditionaly依赖于比较
，列举在根据日K

可以构建找到每一个证据，这些位在源代码的码位，和部分次序键容器缠循环如果你找到他们所有人，声称你有证据表明泡沫排序。

要做到这一点具体的，你需要的标准程序分析机械：

解析源代码和生成抽象语法树
构建符号表（ST），其知道每个标识符，其中的类型它用于构建一个控制流图（CFG），以便检查各种可识别的比特是否以适当的顺序出现
构造数据流图（DFG），以便您可以确定在一部分算法流程正确地另一部分

[这是一个很大的机器刚上手]

在这里，您可以编写特定的代码程序代码爬过AST，ST，CFG，DFG，以“认识到“每个单独的部分。这很可能是非常混乱的，因为每个识别器都会检查这些结构以获取证据。但是，你可以做到。

这已经够混乱了，而且有趣，所以有很多工具可以做到这一点。

我们的DMS Software Reengineering Toolkit是一个。 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\) \) 
      } 
     } 
    ";

在每一个模式，你可以写数额是多少，所选择的编程语言（“模式域”的具体语法），引用模式签名行中指定的数据流。子模式可以在另一个内部提及;必须通过命名来传递子模式中的数据流。与“普通旧C”不同，你必须明确地传递容器，而不是通过隐式引用;那是因为我们对从模式中的一个地方流到另一个地方的实际值感兴趣。（只是因为代码中的两个地方使用相同的变量，并不意味着它们看到相同的值）。给定这些定义，并要求“匹配bubble_sort”，DMS将访问DFG（绑定到CFG/AST/ST）以尝试匹配模式;在匹配的地方，它会将模式变量绑定到DFG条目。如果它找不到所有的匹配，则匹配失败。

为了完成匹配，上面的每个模式基本上都转换成了它自己的DFG，然后每个模式都使用所谓的子图同构测试与代码的DFG进行匹配。构建模式的DFG需要机器的批次：解析，名称解析，控制和数据流分析，应用于原始语言的代码片段，与各种模式元转义混合使用。子图同构对代码来说“很容易”，但运行起来可能非常昂贵。 DMS模式匹配器保存的是，大多数模式都有许多限制[科技点：他们没有节点]，每个尝试匹配都会失败得很快，或者完全成功。

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

我们已经使用它来从陶氏化学公司的真实工业设备控制器中针对它们特有的Dowtran语言（意味着为Dowtran构建解析器等）构建完整的工厂控制模型提取工具。我们有这个原型为C的版本;数据流分析比较困难。

来源

2015-03-27 11:00:34

源代码逻辑评估

回答

相关问题