SW wykład 13 - Slajd12
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ę
Konstrukcja drugiej składowej okazuje się trudniejsza. W kolejnym kroku podejmujemy decyzję, że zbudujemy tę składową jako instrukcję pętli, oczywiście tak, by była ona poprawna względem zadanych dla niej w pierwszym kroku warunków wstępnego i końcowego.
Chcąc zapewnić spełnienie tego warunku poprawności, podejmując obecną decyzję programistyczną (o budowie tej instrukcji jako instrukcji pętli) musimy podać nie tylko warunek wejścia do ciała pętli i zbudować instrukcję ciała pętli, ale także określić niezmiennik pętli oraz zbiór z relacją dobrze ufundowaną i wyrażenie o wartościach w tym zbiorze, które posłużą nam do dowodu całkowitej poprawności pętli (wykład 12, slajd 14).
