SW wykład 13 - Slajd15
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.
