能否證明函數的正確性帶有副作用

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做了類似的事情來模擬副作用，但沒有將它們作爲語言的一部分，但是大量工作使它更符合人體工程學。）但是因爲可以這樣做，所以我們知道副作用是一種熟知的方法，定義的概念。

這意味着我們可以證明有副作用的語言，只要它們的規範爲我們提供了足夠的信息以知道如何將其中的程序重寫爲狀態傳遞樣式。