Poprawność całkowita
Z Wikipedii
Ten artykuł wymaga dopracowania zgodnie z zaleceniami edycyjnymi. Należy w nim poprawić: formatowanie. Po naprawieniu wszystkich błędów można usunąć tę wiadomość. |
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 20 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.