SW wykład 13 - Slajd18
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ę
Składając w oczywisty sposób wszystkie kroki powyższego procesu konstruowania programu liczącego całkowity pierwiastek kwadratowy liczby naturalnej otrzymujemy program w ramce na slajdzie. Co więcej, otrzymujemy nie tylko ten program, ale także skonstruowany wraz z nim dowód jego poprawności względem pierwotnie zadanych warunków wstępnego i końcowego. Każdy krok konstrukcji programu zawiera też odpowiadający mu krok dowodu jego poprawności. Podsumowaliśmy to tutaj przez podanie odpowiednich asercji, wprowadzanych wraz z decyzjami programistycznymi podejmowanymi w poszczególnych krokach konstrukcji.
W ten sposób zakończona konstrukcja programu kończy też realizację zadania programistycznego, zapewniając poprawność zbudowanego rozwiązania.
