SW wykład 1 - Slajd14
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.
