Poprawność całkowita

Poprawność całkowita i częściowa algorytmu.

WP – warunek początkowy – formuła logiczna definiująca dane wejściowe algorytmu.

WK – warunek końcowy – formuła logiczna definiująca dane wyjściowe algorytmu uzyskane dla danych wejściowych spełniających WP.

Definicje:

1. Algorytm A jest częściowo poprawny względem danego warunku WP i danego warunku WK wtedy i tylko wtedy, gdy dla dowolnych danych wejściowych spełniających warunek WP, jeżeli algorytm A zatrzymuje się, to dane wyjściowe algorytmu spełniają warunek WK.

2. Algorytm A jest całkowicie poprawny względem danego warunku WP i danego warunku WK wtedy i tylko wtedy, gdy dla dowolnych danych wejściowych spełniających warunek WP algorytm A zatrzymuje się i dane wyjściowe tego algorytmu spełniają warunek WK.

Przykład:

 WP:    n>0  n N
 WK:    s=1+3+5+...+n  n mod 20  s=1+3+5+...+n-1  n mod 2=0

Algorytm:

 s:=0; i:=1;
 while i<>n+2 do
 begin
        s:=s + i;
        i:=i+2;
 end

Algorytm jest poprawny częściowo, ale nie całkowicie. Dla n parzystego pętla nie ma stopu, ale dla dowolnego n nieparzystego pętla kończy się po skończonej liczbie kroków i wartość końcowa zmiennej s spełnia WK.