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