SW wykład 13 - Slajd17
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ę
Obie składowe instrukcji ciała pętli łatwo już teraz podać wprost, jak na slajdzie powyżej. Weryfikacja ich poprawności względem odpowiednich warunków wstępnego i końcowego jest trywialna (wprost na mocy reguły całkowitej poprawności dla instrukcji przypisania, plus odrobina oczywistych przekształceń arytmetycznych). Łatwo też sprawdzić, że pierwsza składowa zmniejsza wartość wyrażenia , a druga składowa jej nie zmniejsza.
Kończy to konstrukcję w tej gałęzi procesu budowania programu.
