[mazzy]

Цитата:

Сообщение от AX2009

{Pre(x)}P(x,z){Post(x,z)}
Доказательство полной корректности обычно состоит из двух независимых этапов - доказательства частичной корректности и доказательства завершаемости программы

И это называется Верификация.
ищите в яндексе, гугле.
http://ru.wikipedia.org/wiki/%D0%92%...86%D0%B8%D1%8F
есть и книги http://market.yandex.ru/model.xml?hi...37912531229085