1

X给定一大块命令式代码（和周围的程序），是否有一种算法可以确定该代码是否是引用透明的？

到目前为止，我所拥有的是：

一段代码是 RT 如果

  1. 在控制流离开 X 后，不会读取在 X 中分配给的非参考变量

  2. 所有在 X 中被取消引用和分配的引用变量都可以证明是引用遵循规则 1 的变量

  3. 不读取变量或调用函数，其值取决于运行时状态（即scanf(), time(), argv）

编辑：见评论

该算法的完美准确性不是绝对必要的，但它是可取的。（这是现实生活，不是 CS 课，所以有人说，“简单比正确要好一些。”）

编辑2：

没有引用或指针的简化语言的算法草图/想法，表示为抽象语法树：

  1. 查找因果对（即变量的分配和使用）
  2. 对于每一对，将 AST 中的父节点标记为非 RT，直到但不包括最低的共同祖先。

问题：初始化器怎么办？它们算作作业吗？

4

2 回答 2

2

是否可以确定两段代码通常是否具有引用透明性？没有为什么？因为没有程序分析可以完全准确（证明：大量不同的公式，基本上是停机问题）。但是，您可以是近似的。一般来说，有一些技术可以证明哪些类型的程序绝对是参照透明的（因为我们在不近似的保守方面犯了错误，必然会有一些程序是正确的，但不能证明是正确的）：

  • 首先，您需要修复一种语言。分析取决于语言，分析的复杂性将根据您的语言所具有的内容而发生很大变化：并发、引用、指针，所有这些都难以处理。（引用和指针是不一样的，一般来说处理任意指针算术会比简单的引用更难！）
  • 您可以查看一些定理证明器或模型检查器。这些工具可用于检查两个程序是否具有相同的输出，方法是导出对程序建模的公式，然后尝试确定它们是否描述了相同的行为集。
  • 分离逻辑是一种非常流行且不断发展的技术，用于在存在指针的情况下证明两个命令式程序正确。基本思想是对堆的不相交部分进行组合推理（为什么这么好？考虑您编写一个链表实现，现在您将它与一些随机写入该链表中间的代码结合起来。这对于验证来说是地狱。 )
  • 在函数世界中，人们试图将等式推理应用于他们的代码。虽然这在命令式程序中并不完全相同，但如果您使用monad对堆断言建模，您可以做类似的事情。

是否有现成的工具可以应用于大型代码库？不，因为大型代码库使用了无法推理的东西（反射、困难的别名类等）。本质上，您的问题简化为某种定理证明，您需要能够证明两个程序是等价的。有大量论文针对子问题解决了这个问题。例如，考虑用玩具语言编写的非常简单的程序（Imp是一个流行的例子！），大量的论文试图解决这样的问题。

于 2012-09-19T01:11:42.373 回答
2

您可能想阅读“效果系统”或“类型和效果系统”，它们是一种用于描述和跟踪计算具有何种副作用的机制。我不确定是否有任何系统能够进行推理而不是依赖效果注释，但至少你应该能够了解你需要担心什么。

于 2012-09-18T20:14:19.593 回答