SW wykład 10 - Slajd1: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 2: | Linia 2: | ||
[[Grafika:sw1000.png|frame|center|]] | [[Grafika:sw1000.png|frame|center|]] | ||
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. | |||
Aktualna wersja na dzień 17:03, 10 paź 2006
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.
