слабейшее предусловие

Преобразователи предикатов — расширение логики Флойда-Хоара, сделанное Э. Дейкстрой. Впервые появившись в [1], с помощью этого метода определяется семантика императивного программирования и соответствующего языка. В нём каждой команде языка программирования соответствует преобразователь предиката, т. е. полное функциональное соответствие между двумя предикатами в пространстве состояний программы. Основной преобразователь предикатов в последовательном императивном программировании называется слабейшее предусловие (от англ. weakest precondition), обозначаемый wp(S,R). Здесь S — список инструкций (команд), а R — предикат состояния, называемый также . Результат применения этой функции и даёт нам «слабейшее предусловие» для списка S, прерывающийся когда R будет истинным. Например, , получая предикат-копию R со значением x заменённым на E. Важным вариантом wp является так называемое слабейшее свободное предусловие (weakest liberal precondition — перевод даётся по [2]), обозначаемое wlp(S,R). Свободное предусловие является более слабым, т. е. получаемый результат (конечное состояние, удовлетворяющее R) не обязательно «правильный» — гарантируется лишь, что система не выдаст «неправильного» результата (не достигнет такого конечного состояния, которое не удовлетворяло бы R), однако не исключает возможность незавершения работы системы. Таким образом, выражение , где Т — терминальное (конечное) состояние системы, всегда обеспечит истинность R. С помощью wp Дейкстра определил альтернативный (if) и итерационный (do) операторы, а также оператор композиция . Назначением указанных преобразователей предикатов сам Дейкстра указывал создание методологии для программистов по разработке «правильно построенных» программ. Стиль программирования Дейкстры был развит в логике высшего порядка в статье . Можно отметить также другой предикат — сильнейшее постусловие, описывающий максимально сильные ограничения на состояние программы S, которые могут быть получены при данном предусловии.