SW wykład 13 - Slajd11: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1310.png|frame|center|]] | [[Grafika:sw1310.png|frame|center|]] | ||
W kolejnym kroku zajmijmy się konstrukcją pierwszej ze składowych | |||
instrukcji -- jest to pierwsze z (pod)zadań programistycznych, które | |||
wprowadziliśmy w poprzednim kroku. Mamy zbudować instrukcję całkowicie | |||
poprawną względem zadanych warunków wstępnego i końcowego, jak w | |||
górnej ramce na slajdzie. Nie ma co udawać, że jest to zadanie | |||
złożone: dwie oczywiste instrukcje przypisania dają rozwiązanie, | |||
którego poprawność łatwo zweryfikować korzystając z reguł dowodzenia | |||
całkowitej poprawności dla instrukcji złożonej i przypisania. | |||
Zamyka to tę gałąź konstrukcji programu. | |||
Aktualna wersja na dzień 19:05, 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ę
W kolejnym kroku zajmijmy się konstrukcją pierwszej ze składowych instrukcji -- jest to pierwsze z (pod)zadań programistycznych, które wprowadziliśmy w poprzednim kroku. Mamy zbudować instrukcję całkowicie poprawną względem zadanych warunków wstępnego i końcowego, jak w górnej ramce na slajdzie. Nie ma co udawać, że jest to zadanie złożone: dwie oczywiste instrukcje przypisania dają rozwiązanie, którego poprawność łatwo zweryfikować korzystając z reguł dowodzenia całkowitej poprawności dla instrukcji złożonej i przypisania.
Zamyka to tę gałąź konstrukcji programu.
