SW wykład 13 - Slajd12

<<powrót do strony wykładu

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).