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

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

Понятия "сильнее" и "слабее" пришли из логики. Говорят, что 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] для детального знакомства с этими концепциями.

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

Поделитесь на страничке

Следующая глава >

Похожие главы из других книг:

11.4. Условия и циклы

Из книги автора

11.4. Условия и циклы Редко какая-либо программа или сценарий имеют линейный алгоритм. Обычно в ходе работы часто проверяются различные условия и в зависимости от результата принимаются какие-то решения. Для автоматизации работы в коде также используются циклы, которые


Ожидание условия

Из книги автора

Ожидание условия Простое ожиданиеint pthread_cond_wait(pthread_cond_t* cond, pthread_mutex_t* mutex);Вызов функции блокирует вызвавший поток на условной переменной cond и разблокирует мьютекс mutex. Поток блокируется до тех пор, пока другой поток не вызовет функцию разблокирования на условной


Выполнение условия

Из книги автора

Выполнение условия Штатным способом разблокирования потока, блокированного на условной переменной, является вызов функции, сигнализирующей о выполнении условия. В native API это функция SyncCondvarSignal(), которая имеет две POSIX-обертки: pthread_cond_signal() и pthread_cond_broadcast(). Разница между ними


Предварительные условия

Из книги автора

Предварительные условия Данное руководство предполагает наличие у читателя начальных сведений о Linux/Unix, языке сценариев командной оболочки. Кроме того, вы должны знать – как пересобрать ядро операционной системы и иметь некоторое представление о его внутреннем


Условия насыщения

Из книги автора

Условия насыщения Необходимо предварительное замечание перед исследованием условий смещения, приводящих к насыщению транзистора. Из теоретического курса, посвященного изучению транзисторов, вы должны вспомнить, что значения hFE в активной области и в области насыщения


Начальные условия

Из книги автора

Начальные условия Некоторые группы ключевых процессов содержат ключевые практики, отражающие потребность в начальных условиях. Так, например, для «Отслеживания хода проекта и контроля над ним» начальным условием является план разработки ПО. В некоторых случаях


R.5.16 Операция условия

Из книги автора

R.5.16 Операция условия выражение-условия: логическое-выражение-ИЛИ логическое-выражение-ИЛИ ? выражение : выражение-условияУсловные выражения выполняются слева направо. Первое выражение должно быть арифметического типа или типа указателя. Оно вычисляется, и, если


5.2.8. Условия и драйверы

Из книги автора

5.2.8. Условия и драйверы Некоторые условия могут требовать специфической обработки. Эти условия могут касаться ошибок или общего управления потоком данных внутри


ОПЕРАЦИЯ УСЛОВИЯ: ?:

Из книги автора

ОПЕРАЦИЯ УСЛОВИЯ: ?:      В языке Си имеется короткий способ записи одного из видов оператора if-else. Он называется "условным выражением" и использует операцию условия - ?:. Эта операция состоит из двух частей и содержит три операнда. Ниже приводится пример оператора с помощью


Условия поиска

Из книги автора

Условия поиска Возможность конструировать "формулы" для задания условий поиска при выборе наборов, локализации строк при изменениях и удалениях, а также применение правил для создания входных данных является фундаментальной характеристикой языка запросов. Выражения


Условия поиска и упорядочивания

Из книги автора

Условия поиска и упорядочивания Обратите внимание в предыдущем примере, что условия поиска возможны в каждой объединяемой спецификации SELECT. Они являются обычными выражениями поиска, которые должны соответствовать объединяемому набору, управляемому текущим выражением


Условия для изменения OIT и OAT

Из книги автора

Условия для изменения OIT и OAT Каждый раз, когда сервер стартует другую транзакцию, он проверяет состояние идентификаторов транзакций, которые он хранит в TSB, удаляя те, чье состояние было изменено на "подтвержденное", и заново вычисляет значения OIT и OAT. Он сравнивает их с


4.1 Необходимые условия для тестирования

Из книги автора

4.1 Необходимые условия для тестирования 4.1.1 Наличие компонентов продукта Для тестирования пакета программ должны иметься в наличии все его поставляемые компоненты (см. 3.1.2 h), а также нормативные документы, указанные в описании продукта (см. 3.1.2