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

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

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

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

Формула корректности (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, если у него есть возможность выбора? Возможность усиления предусловия означает, что можно предъявлять более жесткие требования к работодателю, в том смысле что можно уменьшить число ситуаций, в которых следует приступать к выполнению работы. Так что сильное предусловие это "хорошие новости" для работника. Наилучшей для него работой - является работа,

{False} A {...} (1)

Постусловие здесь не специфицировано, поскольку не имеет значения каково оно. К выполнению работы можно вообще не приступать, поскольку нет ни одного начального состояния, в котором предусловие было бы истинным. Так что если вам предложат такие условия, немедленно соглашайтесь, не глядя на постусловие, то есть на требования, которые предъявляются к выполненной работе.

Для постусловия ситуация меняется на противоположную. Лучшими для работника являются более слабые условия - это "хорошие новости"; в этом случае хорошо нужно уметь делать очень немногое. В этом случае наилучшей работой - является работа, заданная следующей спецификацией:

{...} A {True} (2)

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

Кстати, почему эта работа является все-таки второй по предпочтительности? Причина, как можно видеть из определения триады Хоара, в завершаемости ( terminate ).

Для случая (1), где нет состояний, удовлетворяющих P, не имеет значения, что делает А, даже если программный текст приводит к выполнению бесконечного цикла, или ломает компьютер. Любое А будет корректным по отношению к данной спецификации.

Для случая (2), однако, требуется завершение работы, должно существовать заключительное состояние, не важно, что делает А, но то, что делается, должно быть выполнено за конечное время.

Обсуждение того, будет ли усиление или ослабление утверждений "хорошей" или "плохой" новостью, шло с позиций работника, нанимающегося для выполнения работы. Обратим ситуацию, и рассмотрим ее с позиций работодателя. В этом случае слабое предусловие станет "хорошей" новостью, поскольку означает выполнение работы для большего множества входных случаев; более предпочтительным теперь является сильное постусловие, поскольку оно расширяет возможность получения важных результатов. Эта двойственность критериев типична в рассмотрении корректности ПО.

Она вновь появится в качестве центрального понятия при обсуждении темы: контракты между модулями - клиентами и поставщиками, в установлении которых преимущества, приобретаемые одним участником, становятся обязательствами для другого.

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