SW wykład 1 - Slajd14: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 1 wersji utworzonej przez jednego użytkownika) | |||
| Linia 2: | Linia 2: | ||
[[Grafika:sw0113.png|frame|center|]] | [[Grafika:sw0113.png|frame|center|]] | ||
Uzasadnienie, że program rzeczywiście oblicza część całkowitą | |||
pierwiastka drugiego stopnia z nieujemnej liczby całkowitej, w istocie | |||
zawieraja wplecione powyżej w tekst programu asercje --- warunki, | |||
które są zawsze spełnione, gdy obliczenia programu znajdą się w | |||
danym "punkcie". Jak jednak właściwie można uzasadnić, że podane | |||
asercje są wystarczające i rzeczywiście pokazują żądaną własność | |||
programu? Przecież nie tylko mogliśmy się pomylić w tym właśnie | |||
przykładzie, ale także przy nieformalnym rozumieniu programu, asercji | |||
i sposobu, w jaki uzasadniają one odpowiednie własności programów. | |||
Aktualna wersja na dzień 09:53, 27 wrz 2006
Wstęp Literatura Programy Programy, sprzeczne oczekiwania WielkiCel Składnia Semantyka Pragmatyka Logika Metodyka Implementacja Formalna semantyka Przykład Przykład, c.d. Przykład, reguła dowodzenia Uzasadnianie poprawności Plan zajęć
Uzasadnienie, że program rzeczywiście oblicza część całkowitą pierwiastka drugiego stopnia z nieujemnej liczby całkowitej, w istocie zawieraja wplecione powyżej w tekst programu asercje --- warunki, które są zawsze spełnione, gdy obliczenia programu znajdą się w danym "punkcie". Jak jednak właściwie można uzasadnić, że podane asercje są wystarczające i rzeczywiście pokazują żądaną własność programu? Przecież nie tylko mogliśmy się pomylić w tym właśnie przykładzie, ale także przy nieformalnym rozumieniu programu, asercji i sposobu, w jaki uzasadniają one odpowiednie własności programów.
