SW wykład 12 - Slajd22: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1221.png|frame|center|]] | [[Grafika:sw1221.png|frame|center|]] | ||
Prosty przykład: dobrą specyfikacją znanego nam programu obliczającego | |||
całkowity pierwiastek kwadratowy liczby naturalnej jest wymaganie, by | |||
był on poprawny względem zwykłego warunku wstępnego (<math>n</math> | |||
jest liczbą naturalną) i binarnego warunku końcowego, który mówi, że | |||
zmienna <math>rt</math> w stanie końcowym ma wartość całkowitego | |||
pierwiastka kwadratowego wartości zmiennej <math>n</math> w stanie | |||
początkowym. Oczywiście, uniemożliwia to akceptację "rozwiązania" | |||
zmieniającego wartość zmiennej <math>n</math> i określającego wartość | |||
<math>rt</math> jako całkowity pierwiastek kwadratowy z nowej wartości | |||
zmiennej <math>n</math>. | |||
Aktualna wersja na dzień 22:13, 16 paź 2006
Zadanie programistyczne Przykład Problemy z logiką Hoare'a Poprawność całkowita Poprawność całkowita, c.d. Poprawność całkowita, c.d. Reguła dla pętli Poprawność systemu dowodzenia dla Tiny Pełność systemu dowodzenia dla Tiny Przykład Uogólnienie Poprawność i pełność Relacje dobrze ufundowane Dowodzenie poprawności całkowitej Przykład Przykład Kolejny problem Binarne warunki końcowe Warunki poprawności Reguły dowodzenia Reguły dowodzenia, c.d. Przykład Logika algorytmiczna System dowodzenia
Prosty przykład: dobrą specyfikacją znanego nam programu obliczającego całkowity pierwiastek kwadratowy liczby naturalnej jest wymaganie, by był on poprawny względem zwykłego warunku wstępnego ( jest liczbą naturalną) i binarnego warunku końcowego, który mówi, że zmienna w stanie końcowym ma wartość całkowitego pierwiastka kwadratowego wartości zmiennej w stanie początkowym. Oczywiście, uniemożliwia to akceptację "rozwiązania" zmieniającego wartość zmiennej i określającego wartość jako całkowity pierwiastek kwadratowy z nowej wartości zmiennej .
