Io-1-wyk-Slajd95

Dowodzenie poprawności programów

Do lat 90-tych dowodzenie poprawności programów odbywało się jedynie dla bardzo krótkich programów. W ciągu ostatniej dekady nastąpił istotny postęp i powstały bardzo efektywne weryfikatory. Jednakże dowodzenie poprawności programu jest wciąż bardzo pracochłonne. Ciekawe dane pozyskano w ramach projektu VSE (Verification Support Environment) finansowanego przez Unię Europejską. Jak pisze prof. Wolfgang Reif, dowiedzenie poprawności programu zawierającego ok. 7 tys. wierszy wymagało pracochłonności około 2 osobolat, a sama specyfikacja formalna miała ok. 5 tys. wierszy tekstu. Jak więc widać, formalna specyfikacja programów może być bardzo obszerna i jej wytworzenie oraz sprawdzenie jej poprawności jest zadaniem samym w sobie.

<< Poprzedni slajd | Spis treści | Następny slajd >>