SW wykład 13 - Slajd17: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1316.png|frame|center|]] | [[Grafika:sw1316.png|frame|center|]] | ||
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 <math>n-rt</math>, a | |||
druga składowa jej nie zmniejsza. | |||
Kończy to konstrukcję w tej gałęzi procesu budowania programu. | |||
Aktualna wersja na dzień 19:15, 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ę
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.
