SW wykład 1 - Slajd15: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 2 wersji utworzonych przez 2 użytkowników) | |||
| Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 1}} | |||
[[Grafika:sw0114.png|frame|center|]] | [[Grafika:sw0114.png|frame|center|]] | ||
Typowy przykład fragmentu uzasadnienia poprawności powyższego | |||
programu to zapisany powyżej, w pierwszej ramce, schemat własności | |||
poprawności instrukcji przypisania: warunek zachodzi po wykonaniu | |||
przypisania, jeśli tylko przed wykonaniem przypisania zachodzi tenże | |||
warunek z przypisywanym wyrażeniem wstawionym za wszystkie wystąpienia | |||
zmiennej, na którą przypisujemy nową wartość (jedną z instancji tego | |||
schematu, wykorzystywaną w przykładzie, pokazujemy powyżej). Ta | |||
intuicyjnie przecież dość oczywista reguła nie jest jednak poprawna | |||
bez dodatkowych założeń. Zachęcamy Państwa do podania przykładów | |||
warunków i instrukcji przypisania w języku Pascal, dla których podana | |||
reguła okazuje się niepoprawna --- można takich istotnie różnych | |||
sytuacji znaleźć bodaj kilkanaście! | |||
Wniosek stąd jeden: każda, nawet pozornie najbardziej oczywista | |||
argumentacja, wymaga formalnych podstaw i ścisłego uzasadnienia. | |||
Aktualna wersja na dzień 09:56, 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ęć
Typowy przykład fragmentu uzasadnienia poprawności powyższego programu to zapisany powyżej, w pierwszej ramce, schemat własności poprawności instrukcji przypisania: warunek zachodzi po wykonaniu przypisania, jeśli tylko przed wykonaniem przypisania zachodzi tenże warunek z przypisywanym wyrażeniem wstawionym za wszystkie wystąpienia zmiennej, na którą przypisujemy nową wartość (jedną z instancji tego schematu, wykorzystywaną w przykładzie, pokazujemy powyżej). Ta intuicyjnie przecież dość oczywista reguła nie jest jednak poprawna bez dodatkowych założeń. Zachęcamy Państwa do podania przykładów warunków i instrukcji przypisania w języku Pascal, dla których podana reguła okazuje się niepoprawna --- można takich istotnie różnych sytuacji znaleźć bodaj kilkanaście!
Wniosek stąd jeden: każda, nawet pozornie najbardziej oczywista argumentacja, wymaga formalnych podstaw i ścisłego uzasadnienia.
