Русская Википедия:Слабейшее предусловие
Преобразователи предикатов — расширение логики Флойда-Хоара, сделанное Э. Дейкстрой. Впервые появившись в [1][1], с помощью этого метода определяется семантика императивного программирования и соответствующего языка. В нём каждой команде языка программирования соответствует преобразователь предиката, т. е. полное функциональное соответствие между двумя предикатами в пространстве состояний программы.
Основной преобразователь предикатов в последовательном императивном программировании называется слабейшее предусловие (от Шаблон:Lang-en), обозначаемый wp(S,R)[2]. Здесь S — список инструкций (команд), а R — предикат состояния, называемый также постусловие. Результат применения этой функции и даёт нам «слабейшее предусловие» для списка S, прерывающийся когда R будет истинным. Например,
- <math> wp(x := E, R)\ =\ R_E^x </math>,
получая предикат-копию R со значением x заменённым на E.
Важным вариантом wp является так называемое слабейшее свободное предусловие (weakest liberal precondition — перевод даётся по [2][2]), обозначаемое wlp(S,R). Свободное предусловие является более слабым, т. е. получаемый результат (конечное состояние, удовлетворяющее R) не обязательно «правильный» — гарантируется лишь, что система не выдаст «неправильного» результата (не достигнет такого конечного состояния, которое не удовлетворяло бы R), однако не исключает возможность незавершения работы системы.
Таким образом, выражение
- <math> wp(S, R)\ =\ ( wlp(S, R)\ and\ wp(S, T))</math>,
где Т — терминальное (конечное) состояние системы, всегда обеспечит истинность R.
С помощью wp Дейкстра определил альтернативный (if) и итерационный (do) операторы, а также оператор композиция (;).
Назначением указанных преобразователей предикатов сам Дейкстра указывал создание методологии для программистов по разработке «правильно построенных» программ. Стиль программирования Дейкстры был развит в логике высшего порядка Ральфа-Йохана Бэка в статье Refinement Calculus[3].
Можно отметить также другой предикат — сильнейшее постусловие, описывающий максимально сильные ограничения на состояние программы S, которые могут быть получены при данном предусловии.
Влияние метода
Лесли Лампорт предложил использовать преобразователи предикатов win и sin для параллельного программирования.[4]
Примечания
Ссылки
Шаблон:Math-stub Шаблон:Compu-stub
- ↑ Дейкстра Э. Guarded commands, nondeterminacy and formal derivation of programs.
- ↑ 2,0 2,1 Дейкстра Э. Дисциплина программирования (A discipline of programming) — 1-е изд. — М.: Мир, 1978. — С. 275.
- ↑ Шаблон:Ref-en Ralph-Johan Back and Joakim von Wright, Refinement Calculus: A Systematic Introduction, 1st edition, 1998. ISBN 0-387-98417-8.
- ↑ Шаблон:Ref-en Leslie Lamport, "win and sin: Predicate Transformers for Concurrency". ACM Transactions on Programming Languages and Systems, 12(3), July 1990. -- Библиография Лесли Лампорта Шаблон:Wayback на сайте Microsoft
