SW wykład 10 - Slajd1
Poprawność programów i weryfikacja Poprawność programów Dowodzenie poprawności Wyspecyfikowany program Logika Hoare'a Definicje formalne Definicje formalne, c.d. Semantyka logiki Hoare'a Reguły wnioskowania Przykład dowodu Przykład dowodu, c.d. Niezmiennik pętli Przykład dowodu, c.d. W pełni wyspecyfikowany program Teorie pierwszego rzędu
Przypomnijmy wstępne rozważania z wykładu 1 (slajd 3) dotyczące programów i ich pożądanych cech. Argumentowaliśmy wtedy, że bodaj najważniejszą, a pewno i najmniej docenianą, cechą programów, którą powinniśmy zapewnić, jest ich poprawność. Tej właśnie własności programów poświęcimy kolejne wykłady.
Dla rozważań o poprawności programów nie wystarcza jednak mówienie o samych programach. Ta własność nie ma sensu dopóki nie wprowadzimy jakiegoś punktu odniesienia, jakiegoś ścisłego kryterium względem którego nasze programy mają być poprawne. Tych kryteriów dostarczają formalne specyfikacje programów.
