ALG7

1.5. Poprawność algorytmów 27

{warunki wstępne'¹} poszukiwany-program {warunki końcowe}

Możliwe jest przy pewnej dozie doświadczenia wyprodukowanie ciągu instrukcji, które powodują przejście z „warunków wstępnych" do „warunków końcowych” - wówczas formalny dowód poprawności algorytmu jest zbędny. Można też podejść do problemu z innej strony; mając dany zespól warunków wstępnych i pewien program: czy jego wykonanie zapewnia „ustawienie" pożądanych warunków końcowych?

Czytelnik może nieco się obruszyć na ogólnikowość powyższego wywodu, ale jest ona wymuszona przez „rozmiar" lematu, który wymaga w zasadzie osobnej książki! Pozostaje zatem tylko ponowić zaproszenie do lektury niektórych zacytowanych wyżej pozycji bibliograficznych - niestety w momencie pisania tej książki niedostępnych w polskich wersjach językowych.

⁴ Wartości zmiennych, pewne warunki logiczne je wiążące etc