SW wykład 13 - Slajd4: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 1 wersji utworzonej przez jednego użytkownika) | |||
| Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 13}} | {{Semantyka i weryfikacja programów/Wykład 13}} | ||
[[Grafika: | [[Grafika:sw1303.png|frame|center|]] | ||
Pozostaje drugi, równie ważny krok rozwiązania: weryfikacja | |||
zaproponowanego programu --- dowód, że jest on rzeczywiście | |||
(całkowicie) poprawny względem specyfikacji zadanej parą warunków | |||
(jak na poprzednim slajdzie). Mamy więc udowodnić stwierdzenie o | |||
całkowitej poprawności programu podane na tym slajdzie. | |||
Aktualna wersja na dzień 19:02, 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ę
Pozostaje drugi, równie ważny krok rozwiązania: weryfikacja zaproponowanego programu --- dowód, że jest on rzeczywiście (całkowicie) poprawny względem specyfikacji zadanej parą warunków (jak na poprzednim slajdzie). Mamy więc udowodnić stwierdzenie o całkowitej poprawności programu podane na tym slajdzie.
