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

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

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

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

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

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

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

$wp(S,R)=(wlp(S,R)andwp(S,T))$$wp(S,R)\ =\ (wlp(S,R)\ and\ wp(S,T))$,

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

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

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

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

Влияние методаПравить

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

СсылкиПравить

• Спецификация программы и преобразователь предикатов wp