SW wykład 1 - Slajd14: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| 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 | |||
zawierają wplecione powyżej w tekst programu asercje --- warunki, | |||
które są zawsze spełnione, gdy obliczenia programu znajdzie 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. | |||
Wersja z 11:09, 17 sie 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 zawierają wplecione powyżej w tekst programu asercje --- warunki, które są zawsze spełnione, gdy obliczenia programu znajdzie 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.
