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.