Zpo-5-wyk-Slajd20
Z Studia Informatyczne
Predykat noSideEffectsP
Analityczne stwierdzenie, czy wykonanie wskazanego fragmentu kodu (pewnej funkcji) nie powoduje zmiany zachowania programu (modyfikacji wybranej zmiennej Var), okazuje się nierozstrzygalne. Spełnienie tego warunku jest konieczne w przypadku wielu przekształceń refaktoryzacyjnych, dlatego stwierdzenie ich poprawności w dowolnym przypadku okazuje się niemożliwe. Ten przykład pokazuje, że analiza statyczna użyta jako metoda weryfikacji poprawności jest zbyt słabym narzędziem już w przypadku bardzo prostych warunków wstępnych.
