Сильные и слабые условия
Сильные и слабые условия
Понятия "сильнее" и "слабее" пришли из логики. Говорят, что P1 сильнее, чем P2, а P2 слабее, чем P1, если P1 влечет P2 и они не эквивалентны. Каждое утверждение влечет True, и из False следует все что угодно. Можно говорить, что True является слабейшим, а False сильнейшим из всех возможных утверждений.
Давайте взглянем на формулу корректности с позиций человека, собирающегося наняться на работу по выполнению операции А. Каковы с его точки зрения наилучшие предусловие P и постусловие Q, если у него есть возможность выбора? Возможность усиления предусловия означает, что можно предъявлять более жесткие требования к работодателю, что можно уменьшить число ситуаций, в которых следует приступать к выполнению работы. Так что сильное предусловие это "хорошие новости" для работника. Наилучшей для него работой - синекурой является работа, чья спецификация выражается формулой:
Синекура 1
{False} A {...}
Постусловие здесь не специфицировано, поскольку не имеет значения каково оно. К выполнению работы можно вообще не приступать, поскольку нет ни одного начального состояния, в котором предусловие было бы истинным. Так что если вам предложат такую синекуру, немедленно соглашайтесь, не глядя на постусловие - требования, предъявляемые к выполненной работе.
Для постусловия ситуация меняется на противоположную. Лучшими для работника являются более слабые условия - это "хорошие новости"; в этом случае хорошо нужно уметь делать очень немногое. Наилучшей работой - второй синекурой является работа, заданная спецификацией:
Синекура 2
{...} A {True}
Как бы не была выполнена работа, постусловие в этом случае будет истинным по определению. Кстати, почему эта работа является все-таки второй по предпочтительности? Причина, как можно видеть из определения триады Хоара, в завершаемости (terminate). Определение устанавливает, что выполнение должно завершиться в состоянии, удовлетворяющем Q, всякий раз, когда оно начинается в состоянии, удовлетворяющем P. Для синекуры 1, где нет состояний, удовлетворяющих P, не имеет значения, что делает А даже если программный текст приводит к выполнению бесконечного цикла, или ломает компьютер. Любое А будет корректным по отношению к данной спецификации. Для синекуры 2, однако, требуется завершение работы, должно существовать заключительное состояние, не важно, что делает А, но то, что делается, должно быть выполнено за конечное время.
Читатели, знакомые с теорией, могли заметить, что формула {P} A {Q} определяет тотальную (total correctness) или полную корректность, включающую завершаемость наряду с соответствием спецификации. Свойство, устанавливающее, что программа удовлетворяет спецификации при условии ее завершения, известно, как частичная корректность. См. [M 1990] для детального знакомства с этими концепциями.Обсуждение того, будет ли усиление или ослабление утверждений "хорошей" или "плохой" новостью, шло с позиций работника, нанимающегося для выполнения работы. Обратим ситуацию, и рассмотрим ее с позиций работодателя. В этом случае слабое предусловие станет "хорошей" новостью, поскольку означает выполнение работы для большего множества входных случаев; более предпочтительным теперь является сильное постусловие, поскольку оно расширяет получение важных результатов. Эта двойственность критериев типична в рассмотрении корректности ПО. Она вновь появится в качестве центрального понятия этой лекции при обсуждении темы: контракты между модулями - клиентами и поставщиками, в установлении которых преимущества, приобретаемые одним участником, становятся обязательствами для другого. Производство эффективного и надежного ПО проходит через составление контрактов, представляющих возможные наилучшие компромиссы во всех межмодульных коммуникациях клиентов и поставщиков.