Przykład udowodnienia częściowej i całkowitej poprawności algorytmu sumy tablicy z liczbami metoda iteracji pętli.

// Vladimir Poplavskij. Wykladowca
// Suma elementow tablicy
// 2022-10-21

ArraySum(arr, n) {
  i = 0;
  sum = 0;

  while (i < n) {
    sum = sum + arr[i];
    i = i + 1;
  }

  return sum;
}
                       

Q (warunek wstępny ): $ i = 0 $ i $ sum = 0 $

B (warunek zatrzymania): $ while (i < n) $

S (ciało pętli ): $ sum = sum + arr[i]; $ oraz $ i = i + 1; $

R (warunek końcowy): $ \sum_{i=0}^{n} arr[i] $

$Niezmiennik( i, sum ) = 0 \leq i \leq n \space\Lambda\space \sum_{k=0}^{i-1} arr[k]$

• algorytm zatrzyma się, kiedykolwiek zajdzie ${ i \leq len }$ - jest iteracja $ i $ oraz $ n $ skończoną liczbą naturalną
• $ n $ jest stałą i skończoną liczbą naturalną - tak
• wartość zmiennej $ i $ rośnie o 1 w każdej iteracji - tak

1. Przypadek podstawowy: udowodnic, że niezmiennik pętli jest prawdziwy po osiągnięciu pętli
2. Krok indukcii:
   • załóżmy, że niezmiennik i warunek zatrzymania są prawdziwe na końcu dowolnego kroku iteracji (hipoteza indukcji $ P(n-1) $)
   • pokaż, że niezmiennik pozostaje prawdziwy po jednej iteracji $(P(n))$
3. Udowodnic warunek końcowy: argumentuj, że niezmiennik i negacja warunka zatrzymania razem sfinalizujmy stan końcowy programu.

Udowdnimy że niezmiennik pętli jest prawdziwy po osiągnięciu pętli:

1. Na starcie pętli mamy $ i = 0 $ i $ sum = 0 $
2. $Niezmiennik( 0, 0 ) = 0 \leq 0 \leq n \space\Lambda\space \sum_{k=0}^{-1} arr[k]$
3. Obydwa tych założenia są prawdziwe

Przypadek podstawowy jest wypelniony

Nieformalnie

Załóżmy, że niezmiennik i warunek zatrzymania są prawdziwe na końcu dowolnej iteracji, pokaż, że niezmiennik pozostaje prawdziwy po jednej iteracji.

• Na końcu dowolnej iteracji i niezmiennik będący prawdą oznacza, że suma jest sumą pierwszych $ i $ elementów $ arr $.
• Po jeszcze jednej iteracji dodajemy $ arr[i] $ do sumy, dlatego suma staje się suma pierwszych $ i+1 $ elementów $ arr $.
• Aby "naprawić to", musimy zwiększyć $ i $ o $ 1 $
• dokładnie to robi pętla
• więc niezmiennik pętli pozostaje prawdziwy

Formalnie

Załóżmy, że niezmiennik i warunek zatrzymania są prawdziwe na końcu dowolnej iteracji, pokaż, że niezmiennik pozostaje prawdziwy po jednej iteracji.

Indeksu dolnego $ 0 $ używamy dla wartości przed iteracją, a $ 1 $ dla wartości po iteracji.

Zakładamy dwie rzeczy, niezmiennik i warunek zatrzymania przed pętlami

• $Niezmiennik( i_0, sum_0 ) = 0 \leq i_0 \leq n \space\Lambda\space sum_0=\sum_{k=0}^{i_0-1} arr[k]$
• $ i_0 < n $

Musimy udowodnic, ze:
$Niezmiennik( i_1, sum_1 ) = 0 \leq i_1 \leq n \space\Lambda\space sum_1=\sum_{k=0}^{i_1-1} arr[k]$

Udowodnimy te dwie koniunkcje osobno

Konjunkcja 1
$ 0 \leq i_1 \leq n $

• Z ciała pętli, my mamy ze $ i_1 = i_0 + 1 $
• Podstawiamy do konjunkcii i mamy do udowdnenia $ 0 \leq (i_0 + 1) \leq n $
• Lewa strona jest prawda, bo $ 0 \leq i_0 $ ze niezmiennik
• Prawa strona jest prawda, bo $ i_0 \leq n $ ze warunka zatrzymania

Konjunkcja 2
$ sum_1=\sum_{k=0}^{i_1-1} arr[k] $

Z ciala pętli mamy $sum_1 = sum_1 + arr[i_0] $ i $ i_1 = i_0 + 1$
$$ sum_1 = sum_1 + arr[i_0] $$(z ciala pętli) $$ = (\sum_{k=0}^{i_0-1} arr[k]) + arr[i_0] $$(z $Niezmiennik(i_0, sum_0)$) $$ = \sum_{k=0}^{i_0} arr[k] $$ $$ = \sum_{k=0}^{i_1 - 1} arr[k] $$

Sprawdzony konjunkcji 1 i 2, wykonany krok indukcyjny.

Udowodnic, że niezmiennik i negacja warunka zatrzymania razem pozwalają nam podsumować warunek końcowy.

niezmiennik i negacja warunka zatrzymania razem: $$ 0 \leq i \leq n \space\Lambda\space sum=\sum_{k=0}^{i-1} arr[k] \space\Lambda\space i \geq n$$ jedyne co trzeba udowdnic ze 1 i 3 konkjukcii sa prawdziwe gdy $ i = n $ , wtedy mamy $$ i = n \space\Lambda\space sum = \sum_{k=0}^{n} arr[k] $$ Suma wszystkich elementów tablicy $ arr $ jest równa $ sum $.

Warunek końcowy - udowdniony.