SW wykład 13 - Slajd11
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ę
W kolejnym kroku zajmijmy się konstrukcją pierwszej ze składowych instrukcji -- jest to pierwsze z (pod)zadań programistycznych, które wprowadziliśmy w poprzednim kroku. Mamy zbudować instrukcję całkowicie poprawną względem zadanych warunków wstępnego i końcowego, jak w górnej ramce na slajdzie. Nie ma co udawać, że jest to zadanie złożone: dwie oczywiste instrukcje przypisania dają rozwiązanie, którego poprawność łatwo zweryfikować korzystając z reguł dowodzenia całkowitej poprawności dla instrukcji złożonej i przypisania.
Zamyka to tę gałąź konstrukcji programu.
