루프 불변 나는 우리가이 프로그램이 부분적으로 올바른 증명할 수 있도록 루프 불변을 찾기 위해 노력하고있어 일부 정확성

Question

을 증명하기위한 :

{ n >= 1 } pre-condition 
i = 1; 
z = 1; 
while (i != n) { 
    i = i + 1; 
    z = z + i*i; 
} 
{ z = n*(n+1)*(2*n + 1)/6 } post-condition 

정말 붙어입니다. 지금까지 시도한 불변의 일부는 다음과 같습니다

z <= n*(n+1)*(2*n + 1)/6^i <= n 

및

z = i*(i+1)*(2*i + 1)/6^i <= n 

난 정말 몇 가지 조언을 부탁드립니다.

Answer 1

적절한 불변성을 찾으려면 조사 된 함수가 실제로하는 직관력을 가져야합니다. 귀하의 예에서 값 i^2은 누적 기 z에 연속적으로 추가됩니다. 그래서 함수로 계산은 (단지 동안 루프의 처음 몇 반복 손으로하고 일반화를 통과) :

1^2 + 2^2 + 3^2 + 4^2 + 5^2 + ... + n^2 

또는 서면 좀 더 공식적으로

SUM_{i=1}^{n} i^2 

즉, 모든의 합 i의 정사각형은 1에서 n까지이다.

첫눈에 반해 이것은 사용자의 사후 조건과 유사하지 않을 수 있습니다. 그러나, 위의 합 I 의도 사후 조건 추측

(n*(n+1)*(2*n + 1))/6 

같다고 n 유도에 의해 표시 될 수있다. 사후 조건이이 합계와 같다는 것을 알게되었으므로 합계에서 불변량을 읽을 수 있어야합니다.