Io-7-wyk-Slajd16

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Dowodzenie poprawności programów(2)

Dowodzenie poprawności programów(2)


Profesor Hoare zaproponował także podejście do specyfikowania i dowodzenia poprawności programów zwane często logiką Hoare’a. Właściwości programu (lub fragmentu programu) Q opisuje się za pomocą pary predykatów P i R. Predykat P opisuje tzw. warunek wstępny, natomiast R jest warunkiem końcowym. Wyrażenie, które widzimy na slajdzie można przeczytać w następujący sposób: jeżeli jest spełniony warunek P, to po wykonaniu instrukcji Q spełniony będzie warunek R.

Oto bardzo prosty przykład. Jeżeli zmienna X ma wartość n, to po wykonaniu instrukcji przypisania zmiennej Y wyniku funkcji silnia od X, zmienna Y będzie miała wartość n!.

To podejście zostało wykorzystane w praktyce przy definicji języka ANNA służącego do specyfikowania programów zapisanych w języku Ada.


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