testing - 可以证明具有副作用的函数的正确性吗

Question

我正在阅读很多关于算法中“正确性证明”*的内容。

有人说证明适用于算法而不是实现，但大多数时候演示是用代码源完成的，而不是数学。并且代码源可能有副作用。所以，我想知道是否有任何基本原则阻止某人证明不纯函数是正确的。

我觉得这是真的，但不能说为什么。如果存在这样的原则，你能解释一下吗？

谢谢

* 抱歉，如果措辞不正确，不确定哪个好。

Answer 1

答案是，虽然数学没有副作用，但可以对具有副作用的代码进行数学建模。

事实上，我们甚至可以利用这个技巧将不纯代码转换为纯代码（无需首先进行数学运算。因此，代替 (psuedocode) 函数：

f(x) = {
  y := y + x
  return y
}

...我们可以写：

f(x, state_before) = {
  let old_y = lookup_y(state_before)
  let state_after = update_y(state_before, old_y + x)
  let new_y = lookup_y(state_after)
  return (new_y, state_after)
}

...它可以完成同样的事情而没有副作用。当然，必须重写整个程序才能显式传递这些状态值，并且您需要为所有可变变量编写适当的函数lookup_和update_函数，但这在理论上是一个简单的过程。

当然，没有人愿意以这种方式编程。（Haskell 做了类似的事情来模拟副作用而不让它们成为语言的一部分，但是很多工作都让它比这更符合人体工程学。）但是因为它可以做到，我们知道副作用是一个很好的 -定义的概念。

这意味着我们可以证明有关具有副作用的语言的事情，只要它们的规范为我们提供了足够的信息来了解如何将其中的程序重写为状态传递样式。