Проектирование по контракту. Корректность ПО

Введение

С момента реализации принципов проектирования по контракту в промышленном языке программирования прошло уже более десяти лет, но именно сегодня, после появления контрактов на платформе .net началось бурное обсуждение этого явления компьютерным сообществом. Но, как и у любого “популярного” явления (которое автоматически становится популярным для многих разработчиков, если за него берется столь сильный участник мира разработки программного обеспечения, как компания Майкрософт) есть и обратная сторона. В сети стало появляться множество публикаций на тему программирования по контракту, которые имеют мало общего с изначальными принципами заложенными Бертраном Мейером (автором этого принципа и языка программирования Eiffel), либо описывают лишь особенности применения конкретной реализации, при этом уделяя слишком мало внимания целям и идеям, положенным в основу проектирования по контракту (Design by Contract).

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

Теме проектирования по контракту я предполагаю уделить две серии постов. В первой серии постов будут рассмотрены теоретические аспекты проектирования по контракту, которые не привязаны к конкретному языку или технологии и будет полезна любому читателю, а во второй серии будут рассмотрена реализация этого принципа на платформе .Net с помощью библиотеки Code Contracts.

Проектирование по контракту

Проектирование по контракту (Design by Contract) – это установление отношений между классом и его клиентами в виде формального соглашения, недвусмысленно устанавливающие права и обязанности сторон. Только через точное определение для каждого модуля требований и ответственности можно надеяться на достижение существенной степени доверия к большим программным системам [Meyer2005].

Рисунок 1 – Контракты между программными элементами

Но прежде чем продолжить рассмотрение темы контрактов, нужно понять причины, побудившие к исследованию этой темы. Почему сигнатура метода и комментарии недостаточны для построения надежного ПО? Почему недостаточно просто описать свои предположения в комментариях к методу, генерировать исключение или возвращать значение по умолчанию, в случае его нарушения? Для чего нужно что-то изобретать, тем самым усложняя и так не простую жизнь программиста? Чтобы ответить на этот вопрос нужно рассмотреть понятие корректности, на основании которого будут строиться все дальнейшие рассуждения.

Корректность ПО

Предположим, вам дали исходный код некоторого проекта, который состоит из 100 000 строк кода на каком-то языке программирования, например на С, и спрашивают, насколько этот код корректен. Естественно, на изучение такого количества кода уйдет приличное количество времени, но любой опытный разработчик с самого начала задаст один простой вопрос: а что этот код должен делать? Вы попросите спецификацию или еще какой-либо документ, который бы говорил о том, что это за проект и какие задачи он призван решать. Без этого вы сможете найти некорректное использование устойчивых идиом, утечки памяти или ресурсов, явные ошибки или ляпы, но не получив ответ на свой вопрос, вы никак не сможете ответить на исходный вопрос о корректности предоставленного вам проекта в целом.

Рассмотрим более конкретный пример. Что вы можете сказать о следующей функции:

int DoSomething(int y) {

    int x = y / 2;

    return x;

}

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

Приведенный выше пример кода четко показывает, что понятие корректности ПО можно рассматривать только по отношению к некоторой спецификации, в то время, как программный элемент сам по себе не может быть ни корректным, ни не корректным [Meyer2005].

ПРИМЕЧАНИЕ
Корректность – это согласованность программных элементов с заданной спецификацией.
Термин “корректность” не применим к программному элементу, он имеет смысл лишь для пары – “программный элемент и его спецификация”

Формула корректности. Сильные и слабые условия

Помимо неформальных определений, существует математическая нотация, широко применяемая в теории формальной проверки правильности программ.
Пусть A – это некоторая операция, тогда формула корректности (correctness formula) – это выражение вида:

{P} A {Q}

Формула корректности, называемая также триадой Хоара, говорит следующее: любое выполнение А, начинающееся в состоянии, где Р истинно, завершится и в заключительном состоянии будет истинно Q, где A обозначает операцию, P и Q – это утверждения, при этом P является предусловием, а Q – постусловием [Meyer2005].

ПРИМЕЧАНИЕ
Приведенная выше формула корректности определяет полную корректность (total correctness), которая гарантирует завершаемость операции A. Помимо этого существует понятие частичной корректности (partial correctness), которое гарантирует выполнение постусловия Q только при условии завершения выполнения операции A.

Рассмотрим следующую триаду Хоара:

{x = 5} x = x ^ 2 {x > 0}

Эта триада корректна, т.к. если перед выполнением операции x^2, предусловие выполняется и значение x равно 5, то после выполнения этой операции, постусловие (x больше нуля) будет гарантировано выполняться (при условии корректной реализации целочисленной арифметики). Из этого примера видно, что приведенное постусловие не является самым сильным. В приведенном примере самым сильным постусловием при заданном предусловии является {x = 25}, а самым слабым предусловием при заданном постусловии является {x > 0}. Из выполняемой формулы корректности всегда можно породить новые выполняемые формулы, путем ослабления постусловия или усиления предусловия.

Понятие “сильнее” и “слабее” пришли из логики. Говорят, что условие P1 сильнее, чем P2, а P2 слабее, чем P1, если выполнение условия P1 влечет за собой выполнение условия P2, но они не эквивалентны. (Например, условие x > 5 (P1), сильнее условия x > 0 (P2), поскольку при выполнении условия P1 выполняется и условие P2 (ведь, если x больше 5, то, естественно, что x больше 0), при этом эти условия не эквивалентны). Из этого следует, что условие True является слабейшим (поскольку при выполнении любого условия, выполняется условие True), а False – сильнейшим (поскольку по своему определению, любое условие, не равное False когда либо выполняется) (рисунок 2).

Рисунок 2 – Сильные и слабые условия (P1 сильнее P2)

ПРИМЕЧАНИЕ
Введение таких понятий, как сильные и слабые условия необходимы для рассмотрения других тем, в частности, вопросов наследования.