SW wykład 13 - Slajd13: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1312.png|frame|center|]] | [[Grafika:sw1312.png|frame|center|]] | ||
Musimy zatem teraz określić warunek wejścia do ciała pętli, instrukcję | |||
ciała pętli, jej niezmiennik, oraz zbiór z relacją dobrze ufundowaną i | |||
wyrażenie o wartościach w tym zbiorze tak, aby zostały spełnione | |||
cztery wymienione na slajdzie wymagania. Zauważmy, że wymagania te są | |||
wystarczające do pokazania całkowitej poprawności pętli względem | |||
podanych warunków wstępnego i końcowego. | |||
Aktualna wersja na dzień 19:11, 17 paź 2006
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ę
Musimy zatem teraz określić warunek wejścia do ciała pętli, instrukcję ciała pętli, jej niezmiennik, oraz zbiór z relacją dobrze ufundowaną i wyrażenie o wartościach w tym zbiorze tak, aby zostały spełnione cztery wymienione na slajdzie wymagania. Zauważmy, że wymagania te są wystarczające do pokazania całkowitej poprawności pętli względem podanych warunków wstępnego i końcowego.
