SW wykład 13 - Slajd5
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?
