пятница, 7 мая 2010 г.

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

Введение

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

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

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

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

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

Figure1

Рисунок 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).

Figure2

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

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

14 комментариев:

  1. Спасибо за статью.

    Единственное не проставлено где ты ссылаешься на
    [Meyer2009] Meyer B. Touch of Class. Leaning to Program Well with Objects and Contracts. London: 2009

    И в названии книги ошибка Leaning ->Learning.

    И еще на мой взгляд важно, что статическая проверка контрактов в дизайнтайм будет работать только под Visual Studio 2008 Team System, Visual Studio 2010 Premium Edition, or Visual Studio 2010 Ultimate Edition. Так что МС кажется не стремится делать контракты "популярными". Хотя сама команда отписалась на форуме что они вроде бы и не против, чтобы сделать этот функционал более доступным ...

    ОтветитьУдалить
  2. @Kostyak: На вторую книгу я явно не ссылаюсь, но она использовалась в качестве доп. источника.

    Будет вторая часть статьи, посвященная именно Code Contracts (т.е. реализации принципа проектирования по контракту в .NET), вот там об этом и стоит указать о возможности статического анализа только под "дорогими" студиями. Здесь же идут общие сведения, просто примеры я привел не на Eiffel-е, а на Code Contracts, чтобы людей не пугать.

    ОтветитьУдалить
  3. epic fail -> DoSomething() в заданном контексте будет корректен всегда ибо лишь деленее на ноль не допустимо.

    ОтветитьУдалить
  4. устоявшийся термин: "тройки Хоара"

    ОтветитьУдалить
  5. @raxxla: читайте внимательнее. Если спецификация этой функции говорит, что она должна извлекать квадратный корень, а она делит на два? То корректна она или нет? Важно то, что пока мы не знаем, что должна делать функция, мы о ее корректности ничего сказать не можем.

    Функция корректна не тогда, когда она не падает с Access Violation, а тогда, когда она выполняет предназначенную ей задачу.

    ОтветитьУдалить
  6. @e.v.e: Да, действительно, "тройка Хоара" несколько более популярный термин, нежели "триада Хоара". Просто основной источник информации по контрактам книга Бертрана Мейера, а там использовался именно второй вариант перевода.

    ОтветитьУдалить
  7. Напишите, пожалуйста, в конце статьи, что продолжнение, в котором будет рассмотрен пример программрования по контракту в Visual Studio, будет через некоторое время.

    А то статья оставляет чувство незаконченности. Вроде рассказано интересно, а на практике как???

    Спасибо.

    ОтветитьУдалить
  8. @Alex: я во введении написал, что проектировании по контракту я планирую уделить две серии постов. В первой серии постов я расскажу о теории (но с примерами уже на Code Contracts под .NET), а во второй серии - про особенности применения проектирования по контракту на платформе .NET. Но уже после знакомства с теорией можно за полчаса пробежаться по официальной документации Code Contracts и сразу же начать полноценно пользоваться этой библиотекой.

    ОтветитьУдалить
  9. ...а самым слабым предусловием при заданном постусловии является {x > 0}.

    Уточнение. Самым слабым предусловием будет {x != 0}.

    ОтветитьУдалить
  10. И ещё. В тексте встречаются ссылки "[Meyer2005]", а самой библиографической ссылки нигде не вижу.

    ОтветитьУдалить
  11. @Евгений: по поводу предусловия вы совершенно правы. Думаю, что здесь стоит привести другой пример, что-то типа {x=5} x = x + 2 {x > 0}, т.к. в случае с возведением в квадрат самое слабое предусловие не выглядит столь очевидным. Спасибо!

    По поводу ссылок на литературу. Вся литература находится в последней статье ("Мониторинг утверждений во время выполнения"), поскольку это скорее не серия отдельных постов, а одна статья, разбитая на несколько частей.

    ОтветитьУдалить
  12. В приведенном примере самым сильным постусловием при заданном предусловии является {x = 25}, а самым слабым предусловием при заданном постусловии является {x > 0}.

    Кажется, тут ошибка. {x > 0} - не самое слабое предусловие же.

    ОтветитьУдалить
  13. Сергей, а что становится с чистотой кода при использовании контрактов?

    Например, дядя Боб считает, что функции не должны быть длиннее 10 строк, плюс он ненавидит защитное программирование (он говорит об этом в одной из серий Clean Code). Я понимаю, что контракты это совсем другое, но "загаживать" код контракты будут не меньше защитных конструкций.

    Разве я не прав и что вы можете сказать по этому поводу?

    ОтветитьУдалить
  14. @Илья Фофанов: чистота кода с контрактами только увеличивается. Все дело в том, что контракты - это наиболее декларативный способ выражения требований к вызывающему коду, к значениям аргументам и к результатам исполнения методов.

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

    Я не вижу никакой связи между контрактами и количеством строк кода, поэтому тут мне нужен дополнительный контекст, чтобы продолжить общение.

    ОтветитьУдалить