能否证明函数的正确性带有副作用

Question

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

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

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

感谢

*很抱歉，如果措辞是不正确，不知道好一个会是什么。

Answer 1

答案是，虽然在数学中没有副作用，但可以用数学方法模拟有副作用的代码。

事实上，我们甚至可以拉动这一招把不纯的代码转换成纯代码（而不必去到数学在首位所以，而不是（伪码）功能：

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_函数l可变变量，但这是一个理论上直截了当的过程。

当然，没有人想这样编程。 （Haskell做了类似的事情来模拟副作用，但没有将它们作为语言的一部分，但是大量工作使它更符合人体工程学。）但是因为可以这样做，所以我们知道副作用是一种熟知的方法，定义的概念。

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