Poprawność

Jakie znaczenie przypisać zwrotowi program [math]P[/math] jest poprawny? Tak sformułowane zdanie nie może byc ani prawdziwe, ani fałszywe. Brakuje kilku elementów. Nieco lepiej brzmi zdanie program [math]P[/math] jest poprawny ze względu na warunek początkowy [math]\alpha[/math] i warunek końcowy [math]\beta[/math]. Zdanie to należy odczytywać w następujacy sposób:jeśli dane programu [math]P[/math] spełniają warunek poczatkowy [math]\alpha[/math] to obliczenie programu P jest skończone i udane, a jego wynik spełnia warunek końcowy [math]\beta[/math]. Widzimy, że brakuje tu informacji o danych i o obliczeniu. Dane to początkowe wartości zmiennych występujących w programie. Obliczenie programu może wyglądać różnie w różnych środowiskach. Przyjmiemy, że środowiskiem jest struktura danych (inaczej zwana: strukturą algebraiczną, algebrą, dziedziną matematyczną, modelem lub środowiskiem opisanym jako klasa -- w programowaniu obiektowym, lub zestaw pierwotnych typów danych w języku programowania LP).