Сильные и слабые условия

Смысл формулы корректности P A Q

Формула корректности

Выражение спецификаций

 

От неформальных высказываний перейдем к простой математической нотации, принятой в теории формальной проверки правильности программ и имеющей ценность при доказательстве корректности программных элементов.

 

 

Пусть А - это некоторая операция (оператор или тело программы). Формула корректности (correctness formula) - это выражение в форме:

 

P A Q

 

 

Формула выражает свойство, которое может быть или не быть истинным:

Любое выполнение А , начинающееся в состоянии, где P истинно, завершится и в заключительном состоянии будет истинно Q .

Формула корректности, называемая также триадой Хоара, - математическое понятие, а не программистская конструкция. Она не является частью языка программирования и введена для того, чтобы выражать свойства программных элементов. В этой формуле А , как было сказано, обозначает операцию, P и Q - свойства вовлекаемых в рассмотрение сущностей, называемые утверждениями (точный смысл этого термина будет определен ниже). Утверждение P называется предусловием, а Q - постусловием.

С этого момента обсуждение корректности ПО будет связываться не с программным элементом А , а с триадой, содержащей этот элемент А , предусловие P и постусловие Q . Единственной целью становится установление того, что триада Хоара P A Q выполняется (истинна).

Вот пример выполняемой тривиальной формулы, в которой полагается, что x имеет тип integer :

 

x>=9 x:= x+5 x>=13

 

 

Число 13 в постусловии не опечатка. Предполагая корректную реализацию целочисленной арифметики, данная формула действительно выполняется. Если предусловие x>=9 выполняется перед присваиванием, то x>=13 будет истинным по завершении оператора присваивания. Конечно, можно утверждать более интересную вещь: при заданном предусловии сильнейшим, насколько это возможно, будет постусловие x>=14 . В свою очередь, при заданном постусловии x>=13 слабейшим предусловием будет x>=8 . Из выполняемой формулы корректности всегда можно породить новые выполняемые формулы, ослабляя постусловие или усиливая предусловие. Займемся теперь выяснением того, что означают термины "сильнее" и "слабее" в пред- и постусловиях.

 

Понятия "сильнее" и "слабее" пришли из логики. Говорят, что P1 сильнее, чем P2 , а P2 слабее, чем P1 , если P1 влечет P2 и они не эквивалентны. Каждое утверждение влечет True , и из False следует все что угодно. Можно говорить, что True является слабейшим, а False сильнейшим из всех возможных утверждений.

Давайте взглянем на формулу корректности с позиций человека, собирающегося наняться на работу по выполнению операции А . Каковы с его точки зрения наилучшие предусловие P и постусловие Q , если у него есть возможность выбора? Возможность усиления предусловия означает, что можно предъявлять более жесткие требования к работодателю, что можно уменьшить число ситуаций, в которых следует приступать к выполнению работы. Так что сильное предусловие это "хорошие новости" для работника. Наилучшей для него работой - синекурой является работа, чья спецификация выражается формулой: