SW wykład 13 - Slajd15: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1314.png|frame|center|]] | [[Grafika:sw1314.png|frame|center|]] | ||
Budujemy zatem instrukcję, która ma być całkowicie poprawna względem | |||
podanego dla ciała pętli warunku wstępnego (jest nim niezmiennik pętli | |||
wzmocniony o warunek wejścia do ciała pętli) i warunku końcowego (jest | |||
nim niezmiennik pętli) oraz ma zapewniać zmniejszanie wartości | |||
wyrażenia <math>n-rt</math>. | |||
Kolejna decyzja: ciało pętli będzie instrukcją złożoną, z asercją | |||
pośrednią wskazaną w powyższym schemacie. Warunki poprawności | |||
instrukcji ciała pętli i podana asercja pośrednia wskazują warunki | |||
wstępne i końcowe, względem których mają być całkowicie poprawne | |||
pierwsza i druga, odpowiednio, składowa ciała pętli. | |||
Aktualna wersja na dzień 19:14, 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ę
Budujemy zatem instrukcję, która ma być całkowicie poprawna względem podanego dla ciała pętli warunku wstępnego (jest nim niezmiennik pętli wzmocniony o warunek wejścia do ciała pętli) i warunku końcowego (jest nim niezmiennik pętli) oraz ma zapewniać zmniejszanie wartości wyrażenia .
Kolejna decyzja: ciało pętli będzie instrukcją złożoną, z asercją pośrednią wskazaną w powyższym schemacie. Warunki poprawności instrukcji ciała pętli i podana asercja pośrednia wskazują warunki wstępne i końcowe, względem których mają być całkowicie poprawne pierwsza i druga, odpowiednio, składowa ciała pętli.
