SW wykład 13 - Slajd6
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ę
Podjęta próba dowodu całkowitej poprawności zaproponowanego programu względem zadanej specyfikacji nie powiodła się. Nadal nic nie wiemy: możliwe są dwie zupełnie różne, ale równie niesatysfakcjonujące sytuacje. Po pierwsze, program nie jest poprawny względem zadanej specyfikacji. Po drugie, być może program jest poprawny względem tej specyfikacji, ale nie potrafiliśmy dotychczas tego pokazać. W obu przypadkach, podjętego zadania programistycznego nie możemy uznać za rozwiązane!
W rozważanym przykładzie zachodzi ta pierwsza możliwość: program nie jest poprawny względem zadanych warunków wstępnego i końcowego. Łatwo się o tym przekonać na przykład "testując" podaną instrukcję dla wartości początkowej .
Tak czy inaczej, najlepsze co możemy zrobić, to próbować dalej...
