Интернет магазин китайских планшетных компьютеров

Компьютеры - Слабейшее предусловие

Преобразователи предикатов — расширение логики Флойда-Хоара, сделанное Э. Дейкстрой. Впервые появившись в, с помощью этого метода определяется семантика императивного программирования и соответствующего языка. В нём каждой команде языка программирования соответствует преобразователь предиката, т. е. полное функциональное соответствие между двумя предикатами в пространстве состояний программы.

Основной преобразователь предикатов в последовательном императивном программировании называется слабейшее предусловие, обозначаемый wp. Здесь S — список инструкций, а R — предикат состояния, называемый также постусловие. Результат применения этой функции и даёт нам «слабейшее предусловие» для списка S, прерывающийся когда R будет истинным. Например,

,

получая предикат-копию R со значением x заменённым на E.

Важным вариантом wp является так называемое слабейшее свободное предусловие, обозначаемое wlp. Cвободное предусловие является более слабым, т. е. получаемый результат не обязательно «правильный» — гарантируется лишь, что система не выдаст «неправильного» результата, однако не исключает возможность незавершения работы системы.

Таким образом, выражение

,

где Т — терминальное состояние системы, всегда обеспечит истинность R.

С помощью wp Дейкстра определил альтернативный и итерационный операторы, а также оператор композиция.

Назначением указанных преобразователей предикатов сам Дейкстра указывал создание методологии для программистов по разработке «правильно построенных» программ. Стиль программирования Дейкстры был развит в логике высшего порядка Ральфа-Йохана Бэка в статье Refinement Calculus.

Можно отметить также другой предикат — сильнейшее постусловие, описывающий максимально сильные ограничения на состояние программы S, которые могут быть получены при данном предусловии.