SW wykład 13 - Slajd5: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1304.png|frame|center|]] | [[Grafika:sw1304.png|frame|center|]] | ||
Korzystając z naszego rozumienia programu i intuicji dotyczącej | |||
zakodowanego w zaproponowanej instrukcji rozwiązania, możemy podjąć | |||
próbę przeprowadzenia dowodu --- na przykład przez podanie | |||
odpowiednich asercji, jak na slajdzie powyżej. | |||
Sprawdźmy, czy podane asercje tworzą dowód zgodny z regułami | |||
dowodzenia całkowitej poprawności. Niestety, NIE! Koniunkcja | |||
niezmiennika pętli i negacji warunku wejścia do ciała pętli nie | |||
implikują warunku końcowego. | |||
I co teraz? | |||
Aktualna wersja na dzień 19:03, 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ę
Korzystając z naszego rozumienia programu i intuicji dotyczącej zakodowanego w zaproponowanej instrukcji rozwiązania, możemy podjąć próbę przeprowadzenia dowodu --- na przykład przez podanie odpowiednich asercji, jak na slajdzie powyżej.
Sprawdźmy, czy podane asercje tworzą dowód zgodny z regułami dowodzenia całkowitej poprawności. Niestety, NIE! Koniunkcja niezmiennika pętli i negacji warunku wejścia do ciała pętli nie implikują warunku końcowego.
I co teraz?
