SW wykład 1 - Slajd14: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 4: | Linia 4: | ||
Uzasadnienie, że program rzeczywiście oblicza część całkowitą | Uzasadnienie, że program rzeczywiście oblicza część całkowitą | ||
pierwiastka drugiego stopnia z nieujemnej liczby całkowitej, w istocie | 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 | które są zawsze spełnione, gdy obliczenia programu znajdą się w | ||
danym "punkcie". Jak jednak właściwie można uzasadnić, że podane | danym "punkcie". Jak jednak właściwie można uzasadnić, że podane | ||
asercje są wystarczające i rzeczywiście pokazują żądaną własność | asercje są wystarczające i rzeczywiście pokazują żądaną własność | ||
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.
