루프 불변량 (유도)에 의한 정확성 증명

Question

필자는 사소한 기능 (PHP는 편리함)을 작성했으며 누군가가 유도를 통해 구조를 도울 수 있기를 바랬다.

function add_numbers($max) { 
    //assume max >= 2 
    $index=1; 
    $array=array(0); 
    while ($index != $max) { 
    //invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1 
    $array[$index] = $array[$index-1]+1; 
    $index += 1; 
    } 
} 

만 때문에 [0] I는 목표 판단 0

초기화 되었더라도 각 인덱스의 값이 인덱스 자체와 동일한 것을되는 결과 (이상이어야한다) 불변성 (그 자체가 의심 스러울 지 모르지만, 바라건대 요점을 얻는다)이 k + 1에 대해 유효하다는 것을 증명하기 위해서.

감사

편집 : 예 : 어쩌면이 같은 http://homepages.ius.edu/rwisman/C455/html/notes/Chapter2/LoopInvariantProof.htm

Answer 1

뭔가,이 조금 현학적이지만.

불변 식 : n> = 1 인 경우 (조건을 검사하는 루프 맨 위에 있음), array [i] = i가 0 일 때 < = i < n 일 때.

증명 : 증명은 유도에 의한 것입니다. 기본 경우 n = 1에서 루프는 처음으로 조건을 확인하고, 본문이 실행되지 않았으며, 코드의 앞부분에서 배열 [0] = 0을 보장합니다. invariant가 k까지의 모든 n에 대해 보유한다고 가정합니다. k + 1의 경우, array [k] = array [k-1] + 1을 할당한다. 유도 가설에서 array [k-1] = k-1이므로 array [k]의 값은 (k-1) +1 = k. 따라서 불변량은 다음, 그리고 모든 유도에 의해 n의 값 (루프 상단)을 유지합니다.

EDIT :

function add_numbers($max) { 
    //assume max >= 2 
    $index=1; 
    $array=array(63); 
    while ($index != $max) { 
    //invariant: ∀ k:1 .. index-1, array[k]=array[k-1]+1 
    $array[$index] = $array[$index-1]+1; 
    $index += 1; 
    } 
} 

불변 : 인덱스 N, N- 경우> = 1, 배열 (이 상태를 확인 루프의 상단) 내가] = 1 0 < 대해 63 + = 때 = i < n.

증명 : 증명은 유도에 의한 것입니다. 기본 경우 n = 1에서 루프는 처음으로 조건을 확인하고, 본문이 실행되지 않았으며, 코드의 앞부분에서 array [0] = 63이라는 외부 보증을받습니다. invariant가 k까지의 모든 n에 대해 보유한다고 가정합니다. k + 1에 대해 우리는 array [k] = array [k-1] + 1을 할당한다. 유도 가설에서 배열 [k-1] = (k-1) + 63 = k + [k]는 (k + 62) +1 = k + 63이다. 따라서 불변량은 다음, 그리고 모든 유도에 의해 n의 값 (루프 상단)을 유지합니다.