SW wykład 13 - Slajd2
Zadanie programistyczne Pierwsze podejście Przykład Weryfikacja Przykład Możliwe przyczyny porażki Poprawiony program Przykład dowodu Drugie podejście Wyprowadzanie programu Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Wyprowadzanie programu, c.d. Własność stopu Własność stopu, c.d. Poprawność przez konstrukcję
Niestety, dla wielu programistów najbardziej oczywiste podejście do uporania się z zadaniem programistycznym opisanym przez parę warunków, wstępnego i końcowego, względem których ma być poprawny skonstruowany program, polega na tym, by po ewentualnej chwili refleksji i krótkim zastanowieniu, po prostu wywołać edytor dedykowany wybranemu językowi programowania i napisać program, z nadzieją, że zbudowany program będzie rzeczywiście poprawny --- być może po drobnych modyfikacjach wymuszonych przez niepoprawne wyniki testowania programu na przypadkowo dobranych danych początkowych. Oczywiście, aby tak zbudowany program mógł być przyjęty jako dobre rozwiązanie zadania programistycznego, tę oczekiwaną poprawność programu należy koniecznie uzasadnić, wykorzystując formalny system dowodzenia (całkowitej) poprawności.
Niekiedy, szczególnie dla niewielkich zadań i przy dużym doświadczeniu, wiedzy i praktyce programisty, takie postępowanie może zostać uwieńczone sukcesem. Ale czy zawsze? Zapewne nie...
