Wprowadzenie
Wiemy, jak bardzo nasze życie zaczyna zależeć od komputerów, a dokładniej od programów komputerowych. Chodzi tu nie tylko o wygodę. Niekiedy działanie komputerów ma krytyczne znaczenie, gdy mówimy o takich zastosowaniach jak transport (nie tylko lotniczy), loty kosmiczne, nadzorowanie życia pacjenta w czasie operacji, dozowanie leków. Wszelkie zastosowania komputerów, gdzie trzeba mieć zaufanie do programu sprawiają, że trzeba zapytać z czego wynika nasze zaufanie, że program komputerowy napisany jest dobrze?
Mija właśnie epoka, w której poprawność programu można było ustalić na podstawie słowa honoru danego przez programistę, że się nie pomylił. Typowym zachowaniem programisty po napisaniu programu to oczywiście jego gruntowne przetestowanie. Gruntowne to nie znaczy całkowite. Rzadko bowiem w czasie testowania mamy wyobraźnię tak bogatą, żeby przedstawić sobie wszystkie możliwe sytuacje, szczególnie wtedy, gdy jest ich potencjalnie nieskończenie wiele. Owszem, testy mogą wykazać, że program jest niepoprawny, ale prawie nigdy (poza przypadkami, kiedy liczba przypadków jest skończona i mała – wielka rzadkość) nie mogą wykazać jego poprawności. Informatycy od dawna próbują skonstruować metody wnioskowania o programach i stają się one coraz popularniejsze, szczególnie że raz udowodnione fragmenty programu mogą być włączane do bibliotek jako poprawne moduły, do których już nie trzeba wracać.
Jak zatem udowodnić, że program robi to, o co nam chodzi? Mniej więcej widać, że gdy wykonamy instrukcję i:=i+1 dla \( i=1 \) będziemy mieli \( i=2 \). Czy możliwe jest jednak opracowanie ogólnej teorii? Okazuje się, że dla ogromnej większości algorytmów jesteśmy w stanie udowodnić ich poprawność korzystając z metod logiki opracowanych na początku lat 60-tych XX wieku. Jak się wkrótce okaże, ta teoria nie tylko pozwala udowodnić poprawność algorytmu, ale i daje metodologię wymyślania algorytmów. Za jej pomocą będziemy wiedzieli, na czym się skupić, gdy zaczynamy projektować pętle.