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

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

${\displaystyle wp(x:=E,R)\ =\ R_{E}^{x}}$ ,

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

Важным вариантом wp является так называемое слабейшее свободное предусловие (weakest liberal precondition — перевод даётся по [2] ), обозначаемое wlp(S,R) . Свободное предусловие является более слабым, т. е. получаемый результат (конечное состояние, удовлетворяющее R) не обязательно «правильный» — гарантируется лишь, что система не выдаст «неправильного» результата (не достигнет такого конечного состояния, которое не удовлетворяло бы R), однако не исключает возможность незавершения работы системы.

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

${\displaystyle wp(S,R)\ =\ (wlp(S,R)\ and\ wp(S,T))}$ ,

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

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

Назначением указанных преобразователей предикатов сам Дейкстра указывал создание методологии для программистов по разработке «правильно построенных» программ. Стиль программирования Дейкстры был развит в логике высшего порядка в статье .

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

Влияние метода

Лесли Лампорт предложил использовать преобразователи предикатов win и sin для параллельного программирования .

Примечания

Ссылки

Это заготовка статьи об информационных технологиях и вычислительной технике . Помогите Википедии, дополнив её. Это примечание по возможности следует заменить более точным .