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 做了类似的事情来模拟副作用，但不让它们成为语言的一部分，但是做了大量的工作使其比这更符合人体工程学。)但是因为它可以做到，所以我们知道副作用是一个很好的-定义的概念。

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