Бертран Мейер - Основы объектно-ориентированного программирования

Свойство корректности ПО

Корректность - понятие относительное.

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

[x].Разработка ПО корректного с самого начала, проектируемого так, чтобы быть корректным. Один из создателей структурного программирования Харлан Д. Миллс в семидесятые годы написал статью со знаменательным названием "Как писать корректные программы и знать это". Слово "знать" в данном контексте означает снабжать программу в момент ее написания аргументами, характеризующими корректность.

[x].Значительно лучшее понимание проблемы и достижение ее решения.

[x].Упрощение задачи создания программной документации. Как будет позже показано, утверждения будут играть важную роль в ОО-подходе к документации.

[x].Обеспечение основ для систематического тестирования и отладки.

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

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

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

{P} A {Q}

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

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

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

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

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

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

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

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

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

Синекура 1

{False} A {...}

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

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

Синекура 2

{...} A {True}

Как бы не была выполнена работа, постусловие в этом случае будет истинным по определению. Кстати, почему эта работа является все-таки второй по предпочтительности? Причина, как можно видеть из определения триады Хоара, в завершаемости ( terminate). Определение устанавливает, что выполнение должно завершиться в состоянии, удовлетворяющем Q , всякий раз, когда оно начинается в состоянии, удовлетворяющем P . Для синекуры 1, где нет состояний, удовлетворяющих P , не имеет значения, что делает А даже если программный текст приводит к выполнению бесконечного цикла, или ломает компьютер. Любое А будет корректным по отношению к данной спецификации. Для синекуры 2, однако, требуется завершение работы, должно существовать заключительное состояние, не важно, что делает А , но то, что делается, должно быть выполнено за конечное время.