SW wykład 1 - Slajd15

<<powrót do strony wykładu

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 uzasadnienie 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.