부작용으로 함수의 정확성을 증명할 수 있습니까?

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_ l 가변 변수이지만 이론적으로 간단한 과정입니다.

물론 아무도 이런 식으로 프로그램하고 싶지 않습니다. (하스켈은 언어의 일부분이되지 않으면 서 부작용을 시뮬레이트하기 위해 비슷한 일을하지만, 이것보다 인간 공학적으로 만들 많은 작업이 진행되고있다.)하지만 그렇게 할 수 있기 때문에 부작용은 잘 알려져있다. 정의 된 개념.

이것은 우리가 부작용과 언어에 대한 것을 증명할 수 있다는 것을 의미, 자신의 사양은 국가 통과 스타일로에 프로그램을 다시 작성하는 방법을 알고 충분한 정보를 제공 한한다.