5768085732

Specyfikowanie programów imperatywnych (cd)

Częściowa poprawność programu II względem prewarunku <E> i postwarunku \I/.

S |= $    ' S-U^S' implikuje S' \=

Własność stopu programu n względem prewarunku <£.

S \= $ implikuje 'I' uruchomiony w S kończy działanie

-15-

Wstęp do programowania, M.A.B 2004