Мониторинг утверждений в период выполнения

Это последняя статья из цикла статей о теоретических аспектах проектирования по контракту, в которой рассматриваются уровни мониторинга утверждений во время выполнения, а также роль контрактов в создании документации.

Мониторинг утверждений в период выполнения

Как уже говорилось ранее, поведение системы при нарушении утверждений во время выполнения полностью зависит от разработчика. Механизмы проектирования по контракту предоставляют возможности управлять этим поведением путем задания соответствующих параметров компиляции, тем самым включая и отключая проверки времени выполнения по своему усмотрению.

Перечень подобных настроек определяется используемым языком или библиотекой, а также количеством поддерживаемых утверждений (как уже говорилось ранее, не все реализации принципов проектирования по контракту поддерживают инварианты циклов). Если рассматривать полный перечень утверждений, изначально предложенный Бертраном Мейером в [Meyer2005], то можно выделить следующие уровни мониторинга:

no – во время выполнения нет проверок никаких утверждений. В этом случае утверждения играют роль комментариев;

require – проверка только предусловий на входе методов;

ensure – проверка постусловий на выходе методов;

invariant – проверка выполнимости инвариантов на входе и выходе всех экспортируемых методов;

loop – проверка выполнимости инвариантов циклов;

check – проверка инструкций утверждений;

all – выполнение всех проверок (в языке Eiffel этот уровень мониторинга эквивалентен уровню check);

Каждый последующий уровень автоматически влечет за собой выполнение всех предыдущих. Именно поэтому check и all в языке Eiffel определяют одинаковые уровни мониторинга.

Результат нарушения утверждения в период выполнения также может изменяться в зависимости от параметров компиляции и может различаться в зависимости от реализации. Так, в языке Eiffel нарушение утверждения в период выполнения всегда приводит к генерации исключения, а в библиотеке Code Contracts разработчик может выбрать требуемое поведение; это может быть либо генерация исключения, либо нарушение стандартного утверждения (assertion), что приведет остановке выполнения программы и выдаче пользователю стандартного диалогового окна.

Оптимальный уровень утверждений

Подобная гибкость автоматически приводит к еще одному вопросу: какой уровень мониторинга утверждений во время выполнения является оптимальным? Ответ на него выбирается как компромисс между уровнем доверия к качеству кода и последствиями необнаруженных ошибок в период выполнения.

Существует два простых крайних случая. Во время отладки системы мониторинг утверждений должен быть включен на максимальном уровне, а для систем с высокой степенью доверия к коду, критичных ко времени выполнения мониторинг утверждений может быть отключен полностью. Если первый случай особых вопросов не вызывает, то второй совет звучит весьма неоднозначно. Хотя в настоящее время широко развиваются системы статистического анализа кода, которые благодаря механизму утверждений способны выявить значительное количество ошибок, формальных доказательств корректности кода все еще не существует, поэтому говорить о “полном” доверии к коду вряд ли возможно. Здесь очень уместно высказывания Тони Хоара:

Абсурдно выполнять проверку в период отладки, когда не требуется доверие к получаемым результатам, и отключать ее в рабочем состоянии, когда ошибочный результат может стоить дорого или вообще катастрофичен. Что бы вы подумали о любителе плавания, который надевает спас-жилет во время тренировок на берегу и снимает его, бросаясь в море? [Hoare1973]

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

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

Контракты и документация

Помимо явных преимуществ использования контрактов для создания надежного и расширяемого программного обеспечения, утверждения обладают еще одним важным преимуществом – самодокументированием.

Как уже говорилось ранее, обычно, если спецификация и существует, то является отдельным документом, что является нарушением принципа “Нет избыточности” [Meyer2005] или принципа DRY (Don’t Repeat Yourself) [Hunt2002]. Подобное дублирование информации пагубно по той простой причине, что проблемы рассогласования дублируемой информации является лишь вопросом времени. Как бы ни старалась команда разработчиков (или даже выделенный человек) поддерживать информацию в различных источниках в согласованном состоянии, рано или поздно наступит момент, когда рассогласование информации все же произойдет.

Поскольку проектирование по контракту предполагает содержание элементов спецификации в самом исходном коде, мы получаем единый источник информации о программной системе, вероятность рассогласования которого минимальна.

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

Выводы

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

Литература

1. [Meyer2005] Мейер Б. Объектно-ориентированное конструирование программных систем. М.: Русская редакция, 2005
2. [Meyer2009] Meyer B. Touch of Class. Learning to Program Well with Objects and Contracts. London: 2009
3. [Hoare1981] C.A.R. Hoare: The Emperor’s Old Clothes (1980 Turing Award lecture), in Communications of the ACM, vol. 24, no. 2, February 1981, pages 75-83.
4. [Hunt2000] Хант Э., Томас Д. Программист-прагматик. Путь от подмастерья к мастеру. М.: Лори, 2007
5. [McConnell] Макконнелл С. Совершенный код. 2-е издание. СПб.: Питер, 2005
6. [Howard] Ховард М., Лебланк Д. Защищенный код. 2-е издание. М.: Русская редакция, 2005
7. [Maguire] Maguire, Steve. Writing Solid Code. Redmond, WA: Microsoft Press, 1993
8. [Coplien1992] Джеймс Коплиен. Программирование на С++. Питер, 2005
9. [Hoare1973] C.A.R. Hoare: Hints on Programming Language Design, Stanford University Artificial Intelligence
   

Проектирование по контракту. Наследование

Рассмотренные ранее механизмы взаимодействия между двумя программными элементами моделируют взаимоотношение “использует” (HAS-A relationship) или взаимоотношение типа “клиент-поставщик”. Механизмы наследования, играющие ключевую роль в объектном подходе с точки зрения расширяемости и повторного использования, моделируют взаимоотношение “является” (IS-A relationship) и добавляют взаимоотношения между базовым классом и его потомком.

 
Рисунок 4 – Взаимоотношения между объектами

Опытные разработчики знают, что чрезмерное использование наследования – это один из ключевых факторов, который приводит к созданию сложного в понимании и сопровождении кода. Связано это, прежде всего с тем, что отношение «является» обладает более сильной связью, чем отношение “использует”, и каждый раз, при анализе кода производного класса нужно анализировать поведение всех его базовых классов и четко понимать «контракт», который базовые классы предоставляют своим наследникам. Использование утверждений совместно с наследованием не только упрощает создание производных классов, но и гарантирует клиентам базового класса согласованное поведение при использовании динамического связывания и полиморфизма.

Инварианты

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

ПРИМЕЧАНИЕ
Правило родительских инвариантов: инварианты всех родителей применимы и к самому классу

Инварианты базовых классов добавляются к текущему классу и соединяются логической операцией and. Если базовый класс не содержит явного инварианта, то его роль играет инвариант True. По индукции в классе действуют инварианты всех его потомков, как прямых, так и косвенных.

Предусловия и постусловия

Полиморфизм и динамическое связывание добавляет некоторые особенности при работе с предусловиями и постусловиями.

Давайте рассмотрим гипотетический пример. Предположим у нас есть класс С, который содержит ссылку на класс B. Вследствие динамического связывания, в период выполнения вместо объекта класса B может быть использован объект класса D или любого другого наследника класса B.

Предположим, что в классе B определена открытая функция int Foo(int x), с предусловием x > 5 (pre_b) и постусловием Result > 0 (post_b):

class B {

  public virtual int Foo(int x) {

      Contract.Requires(x > 5, "x > 5");

      Contract.Ensures(Contract.Result<int>() > 0,

                       "Result > 0");

      // Реализация метода

  }

}

Тогда использование объекта класса B внутри класса C может выглядеть следующим образом:

class C {

  //...

  B b = GetFromSomewhere();

  int x = GetX();

  if (x > 5) { //Проверяем предусловие pre_b

    int result = b.Foo(x);

    Contract.Assert(result > 0); // Проверяем постусловие post_b

  }

}

Благодаря проверке предусловия, класс С выполняет свою часть контракта и может рассчитывать на выполнение контракта классом B (или одним из го потомков). Согласно принципу подстановки Лисков [Coplien1992] поведение приведенного фрагмента кода не должно измениться, если во время выполнения динамическим типом объекта B будет один из наследников класса B.

Но что, если при переопределении функции Foo один из наследников класса B захочет изменить предусловия и постусловия?

  
Рисунок 5 – Некорректное переопределение предусловия и постусловия

Давайте предположим, что функция int Foo(int x) в класс D начинает требовать больше (содержит более сильное предусловие вида: x > 10), и гарантировать меньше (содержит более слабое постусловие вида: x > -5):

class D : B {

    public override int Foo(int x) {

        Contract.Requires(x > 10, "x > 10");

        Contract.Ensures(Contract.Result<int>() > -5,

                         "Result > -5");

        return -1;

    }

}

В этом случае, хотя клиент класса B полностью выполняет свою часть контракта и предоставляет входное значение функции Foo, удовлетворяющее предусловию он может не получить требуемого результата. Усиление предусловия означает, что данные корректные для базового класса станут некорректными для его наследника (в нашем примере, это может быть значение x равное 6), а ослабление постусловия означает, что результат, на который рассчитывает клиент базового класса может быть не выполнен классом наследником (в нашем примере, это может быть результат выполнения функции Foo равный -1).

Отсюда можно сделать вывод, что при переопределении методов предусловие может заменяться лишь равным ему или более слабым (требовать меньше), а постусловие – лишь равным ему или более сильным (гарантировать больше). Новый вариант метода не должен отвергать вызовы, допустимые в оригинале, и должен, как минимум, представлять гарантии, эквивалентные гарантиям исходного варианта. Он вправе, хоть и не обязан, допускать большее число вызовов или давать более сильные гарантии [Meyer2005].

class D : B {

    public override int Foo(int x) {

        Contract.Requires(x > 0, "x > 0");

        Contract.Ensures(Contract.Result<int>() > 10,

                         "Result > 10");

        return 25;

    }

}

Ковариантность и контравариантность

Хорошим примером изменения гарантий методов при переопределении является возможность многих языков программирования изменять тип возвращаемого значения при переопределении с базового на производный. Это понятие называется «ковариантность по типу возвращаемого значения» (return type covariance) и выглядит следующим образом:

class B1 {};

class D1 : public B1 {};

class B2 {

public:

  virtual B1 Foo();

};

class D2 : public B2 {

public:

  virtual D1 Foo();

};

  
Рисунок 6 – Ковариантность по типу возвращаемого значения

Эта  возможность (которая поддерживается в C++, Java, D и других языках) полностью согласуется с принципами проектирования по контракту и, в частности, с принципом усиления постусловия, поскольку можно считать, что для типов D1 и B1 выполняется соотношение typeof(D1) < typeof(B1).

  
Рисунок 7 – Отношение порядка между объектами иерархии наследования

Аналогичным примером может служить ковариантность по типу возвращаемого значения и контрвариантность по типу принимаемого значения обобщенных интерфейсов и делегатов в C# 4.0. И хотя в этом случае речь идет не о наследовании, а о совместимости по присваиванию, можно говорить о тех же самых принципах и правилах, что и при переопределении утверждений классами потомками. Так, например, делегату d1 с предусловием pre1 и постусловием post1 может быть присвоен делегат d2 с предусловием pre2, равном pre1 или более слабым, и постусловием post2, равным post1 или более сильным:

void Foo(object obj) {}

string Boo() {return “Boo”;}

 

//...

// Контравариантность аргументов:

// предусловие делегата Action<object> и, соответственно

// метода Foo, слабее предусловия делегата

// Action<string>, поскольку typeof(object) < typeof(string)

Action<string> action = Foo;

// что аналогично следующему коду:

Action<string> action = new Action<object>(Foo);

 

// Ковариантность возвращаемого значения:

// постусловие делегата Func<string> и, соответственно

// метода Boo, сильнее постусловия делегата

// Func<object>, поскольку typeof(string) > typeof(object)

Func<object> func = Boo;

// что аналогично следующему коду:

Func<object> func = new Func<string>(Boo);

Утверждения и защитное программирование

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

Утверждения и проверка входных данных

Проектирование по контракту предназначено для формализации взаимоотношения двух программных элементов внутри доверенной среды и не предназначена для взаимодействия программного элемента с внешним миром. Главный принцип защищенного кода «все входные данные зловредны, пока не доказано противное» [Howard] остается в силе и о нем не следует забывать при разработке любых приложений, не зависимо от того, построены они по принципам проектирования по контракту или без него.

 
Рисунок 3 – Доверенная и ненадежная среда

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

Проектирование по контракту и защитное программирование

Одним из главных принципов проектирования по контракту является отсутствие проверок предусловий внутри тела программы. Это правило противоречит принципам защитного программирования, в котором “открытые методы класса предполагают, что данные небезопасны и отвечают за их проверку и исправление. Если данные были проверены открытыми методами класса, закрытые методы могут считать, что данные безопасны” [McConnell] При этом внутри открытых методов рекомендуется применять обработчики ошибок (например, генерировать исключение или возвращать соответствующий код ошибки, в случае неверных входных данных), а в закрытых методах применять утверждения (assertions) (поскольку это характеризует программные ошибки).

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

Кроме того, в защитном программировании существует негласное правило, согласно которому “лишняя проверка никогда не повредит”, и действительно, если рассмотреть простой пример (например, функцию извлечения квадратного корня double Sqrt(double x)) может показаться, что никакого вреда от дополнительной проверки нет и быть не может, но так ли это на самом деле?

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

Проектирование по контракту идет по пути “чем меньше и конкретнее задача, тем проще разработка, поддержка и сопровождение кода”. “С этой глобальной точки зрения простота становится критическим фактором. Сложность – главный враг качества… Добавляя избыточные проверки, добавляете больше кода. Больше кода – больше сложности, отсюда и больше источников условий, приводящих к тому, что все пойдет не так, это приведет к дальнейшему разрастанию кода и так до бесконечности. Если пойти по этой дороге, то определенно можно сказать одно – мы никогда не достигнем надежности. Чем больше пишем, тем больше придется писать” [Meyer2005].

Автор проектирования по контракту, Бертран Мейер считает, что обеспечение надежности отдельных модулей недостаточно для построения надежного ПО. “Для систем сколь либо существенных размеров недостаточно обеспечение качества отдельных элементов, - более важно гарантировать, что для каждого взаимодействия двух элементов задан явный список взаимных обязательств и преимуществ – контракт”.

Когда контракт нарушается

Мы говорили о том, что поставщик не должен проверять предусловие в своем коде, он может положиться на его выполнение и не рассматривать случаи его нарушения. Но что же произойдет во время выполнения при нарушении контракта и что семантически значит нарушение предусловия, постусловия или инварианта? Давайте попробуем найти ответы на все эти вопросы.
Нарушение контракта означает отклонение конкретной реализации от заданной спецификации, что говорит о некорректности реализации и является проявлением ошибок (или “жучков”) в программном коде.

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

Как мы говорили ранее, инвариант класса можно рассматривать как добавление еще одного утверждения в предусловия и постусловия всех экспортируемых методов класса, и поскольку его соблюдение ложится на поставщика услуги, то нарушение инварианта эквивалентно нарушению постусловия (т.е. это ошибка в коде поставщика).

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

Совместная работа над кодом в компании Google

Во второй главе книги «Coders at Work», Брэд Фицпатрик (Brad Fitzpatrick) — автор Live Journal, а сейчас сотрудник компании Google, помимо всяких интересных баек о создании Live Journal, об учебе и о многом другом, рассказывает и о принципах владения кодом и о совместной работе над ним в компании Google.

Как известно, в Google существует возможность использовать двадцать процентов своего рабочего времени в целях, отличных от целей текущего проекта (но в целях и интересах компании в целом). Это явление называется групплеты (grouplet) (об этом можно почитать в замечательной статье «The Google Way: Give Engineers Room», или в переводе этой статьи здесь), соответственно, у каждого разработчика может появиться дикое желание порыться в чужом коде и поучаствовать в каком-то проекте. А поскольку таких проектов, мягко говоря, много, то требуются некоторые формальные правила, которые позволят поддерживать весь код в актуальном состоянии и не позволят его качеству опускаться ниже определенного уровня.

В Google (по словам Брэда, сам не был, не знаю) весь код хранится в едином репозитории, с одним корнем огромного дерева и каждый человек может получить исходники любого проекта в любой момент времени. На это не накладывается никаких ограничений, т.е. доступ на чтение есть у каждого сотрудника, но это не означает, что любой желающий может залить этот код обратно со своими собственными исправлениями.

Для того, чтобы исправленный код попал обратно в репозиторий должны быть выполнены два требования. Во-первых, вы должны получить «одобрение» от владельца кода (code owner), а во-вторых, одобрение от сертифицированного специалисти по тому языку программирования, который используется в этом проекте (readability approved person) (кстати, совершенно не обязательно, чтобы это были два разных человека, две эти роли вполне могут ужиться и в одном человеке).

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

Анализ кода (readability review), который проводится экспертом по соответствующему языку призван обеспечить прежде всего согласованный стиль написания кода, ведь для любого крупного проекта гораздо важнее единство стиля и минимальное количество «переключений» мозга при чтении с одного стиля на другой. В этом случае на первый план выходит не абсолютная полезность некоторого правила, а его согласованное применение (да, лично я предпочитаю другой формат отступов или формат именования переменных, но гораздо лучше, чтобы стиль форматирования кода был единым, независимо от сотен различных предпочтений различных сотрудников).

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

Кстати, а как обстоят дела дела в вашей компании с владением кода и совместной работой над ним?

Дополнительные ссылки:
Code readability

Проектирование по контракту. Утверждения

Утверждения

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

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

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

Утверждение – это логическое выражение, которое должно быть истинным на некотором участке программы и может включать сущности нашего ПО. Утверждениями могут служить обычные булевы выражения с некоторыми расширениями. Так, в утверждениях помимо булевых выражений могут применяться функции (но с некоторыми ограничениями: это должны быть функции без “побочных эффектов”, т.е. не изменяющие состояние объекта). А для постусловий необходима возможность обратиться к результату выполнения функции, а также к значению, которое было до начала выполнения этой функции (определяется термином “old”).

Большинство современных языков программирования содержат метод assert, который проверяет истинность утверждения во время выполнения и является основой «Защитного программирования». И хотя этот механизм имеет отношение к рассматриваемой теме, он является лишь малой частью тех возможностей, которые доступны благодаря утверждениям в Проектировании по контракту.

ПРИМЕЧАНИЕ
Первым защитником использования утверждений в программировании был никто иной, как сам Алан Тьюринг. На конференции в Кембридже 24 июля 1950 г. он представил небольшой доклад “Проверка больших программ”, в которой объяснял эту идею с большой ясностью. “Как можно проверить большую программу, утверждая, что она правильна? Чтобы для проверяющего задача не была слишком трудной, программист обязан написать некоторые утверждения, которые можно проверить индивидуально, и из которых корректность программы следует достаточно просто” [Hoare 1981]

Предусловия и постусловия

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

Пусть предусловие определяется ключевым словом require, а постусловие – ключевым словом ensure. Тогда, если с некоторой функцией r связаны утверждения require pre и ensure post, то класс говорит своим клиентам следующее [Meyer2005]:

“Если вы обещаете вызвать r в состоянии, удовлетворяющем pre, то я обещаю в заключительном состоянии выполнить post”.

{Pre r} R {Post r}

Классическим примером предусловий и постусловий могут служить функция извлечения квадратного корня Sqrt или методы добавления и удаления элемента из стека:

//Math.cs

public class Math {

    public static double Sqrt(double x) {

        Contract.Requires(x >= 0, "Positive x");

        // Реализация метода

    }

}

 

//Stack.cs

public class Stack<T> {

    public void Push(T t) {

        Contract.Requires(t != null, "t not null");

        Contract.Ensures(Count == Contract.OldValue(Count) + 1,

                         "One more item");

        // Реализация метода

    }

 

    public T Pop() {

        Contract.Requires(Count != 0, "Not empty");

        Contract.Ensures(Contract.Result<T>() != null,

                         "Result not null");

        Contract.Ensures(Count == Contract.OldValue(Count) - 1,

                         "One fewer item");

        // Реализация метода

    }

 

    public int Count {get;}

}

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

Предусловие связывает вызывающий код: определяются условия при которых вызов программы клиентом легитимен (например, x > 0 для функции Sqrt или Count != 0 для функции Pop класса Stack). При этом обязательства клиента приносят выгоду классу-поставщику, поскольку классу, выполняющему операцию, не нужно заботиться о том, что же делать при нарушении предусловия: возвращать значение по умолчанию или код ошибки, генерировать исключение, сохранять информацию об ошибки в поток ввода-вывода или прерывать выполнение программы.
Постусловие связывает класс: определяются условия, которые должны быть выполнены по завершению операции (класс Stack должен обеспечить увеличение количество элементов на 1 после выполнения функции Push). Здесь выгода клиента (результат выполнения функции) оборачивается обязательствами поставщика (он уже не может не выполнить свои обязательства, коль они прописаны в контракте).

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

Поскольку булевы выражения в предусловиях могут ссылаться не только на аргументы, но и на другие компоненты или функции, то существует вероятность использования в предусловии такого выражения, которое не будет доступно клиенту, вызывающую саму функцию.

В приведенном ранее примере предусловия метода Pop класса Stack говорилось о том, что вызов этого метода легитимен только в случае, когда стек не пуст. Давайте предположим, что мы переписали наш класс Stack следующим образом:

// Stack.cs

public class Stack<T> {

    public T Pop() {

        Contract.Requires(Count != 0, "Not empty");

        Contract.Ensures(Contract.Result<T>() != null,

                         "Result not null");

        Contract.Ensures(Count == Contract.OldValue(Count) - 1,

                         "One fewer item");

        // Реализация

    }

    private int Count {get;}

}

В этом случае клиент класса Stack не может самостоятельно удостоверится, удовлетворяет ли он предусловию или нет (поскольку у него нет доступа к проверке предусловия самостоятельно). Чтобы исключить такую проблему существует правило, согласно которому «каждый компонент, появляющийся в предусловии программы, должен быть доступен каждому клиенту, которому доступна сама программа”.

ПРИМЕЧАНИЕ
При использовании библиотеки Code Contracts приведенный выше код компилируется, но компилятор выдает предупреждение вида: warning CC1038: CodeContracts: Member 'get_Count' has less visibility than the enclosing method ' Stack`1.Pop'.

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

Инварианты класса

Предусловия и постусловия характеризуют конкретные функции, но не класс в целом. Экземпляры класса часто обладают некоторым глобальными свойствами, которые должны выполняться после создания объекта и не нарушаться в течение всего времени жизни. Такие свойства носят название инвариантов класса (class invariants) и они определяют более глубокие семантические свойства и ограничения, присущие объектам этого класса.

Такими свойствами могут служить внутренние условия (некоторое поле не равно null или количество элементов неотрицательно) или правила согласованности внутреннего состояния объекта (empty = (count = 0) или deposit_list.total – withdrawals_list.total = balance). Каждое такое условие не связывает конкретные функции, а характеризует объект в каждый устойчивый момент времени.

Инвариант класса должен выполняться после завершения функции создания (конструктора) и между вызовами всех открытых методов. Вполне законно, что некоторая функция в начале своего выполнения разрушает инвариант класса, а перед завершением выполнения – восстанавливает его истинность. При этом выполнение инвариантов должно соблюдаться только между вызовами экспортируемых методов, в то время, как закрытые методы могут вызываться в состоянии, в котором инвариант нарушен и завершать свое выполнение не восстанавливая его истинность.

Утверждение Inv является корректным инвариантом класса, если и только если оно удовлетворяет следующим двум условиям [Meyer2005]:

1) Каждая процедура создания, применимая к аргументам, удовлетворяющим ее предусловию в состоянии, в котором атрибуты имеют значения, установленные по умолчанию, вырабатывает заключительное состояние, гарантирующее выполнение Inv.

2) Каждая экспортируемая процедура класса, примененная к аргументам в состоянии, удовлетворяющем Inv и предусловию, вырабатывает заключительное состояние, гарантирующее выполнение Inv.

Первое условие определяет роль функции создания в жизненном цикле объекта класса и может быть выражено формально следующим образом:

{Default and pre} body {post and Inv}

где Default – состояние объекта некоторого класса со значениями полей по умолчанию (которое зависит от конкретного языка или платформы), pre – предусловие, body – тело конструктора, post – постусловие, Inv – инвариант класса.

Эта формула корректности означает, что любая функция создания (конструктор), при вызове которой выполняется предусловие, должна создать объект, у которого выполняется постусловие и его инвариант. Во многих языках программирования если не задавать явно функцию создания, то она будет создана за вас компилятором. В этом случае, значение объекта по умолчанию (Default) удовлетворяет инварианту класса (Inv).

Второе условие позволяет неявно рассматривать инварианты как добавления к предусловиям и постусловиям, которые действуют на все контракты между классом и его клиентами.

{Inv and pre} body {Inv and post}

где body – тело экспортируемого метода, pre – предусловие, post – постусловие, а Inv – инвариант класса.

Эта формула корректности означает, что любое выполнение метода (body), которое начинается в состоянии, удовлетворяющем инварианту (Inv) и предусловию (pre), завершится в состоянии, в котором выполняются инвариант (Inv) и постусловие (post).

Инструкция утверждения

Помимо предусловий, постусловий и инвариантов бывают ситуации, когда в некоторой точке кода должно выполняться некоторое условие, невыполнение которого означает программную ошибку. Это может быть дополнительная проверка предусловия или постусловия, либо выполнение некоторого условия, которое скажет читателю кода, на каких гипотезах строится его исполнение. Например, это может быть предположение о том, что значение некоторой целочисленной переменной неотрицательное, что ссылка не равна null, индекс не выходит за границы диапазона или контейнер не пуст и т.п.

При использовании рассмотренной ранее функции Sqrt предположение о неотрицательном значении аргумента может быть известно из контекста:

double x = a * a + b * b; //x не может быть отрицательным

// ...

Contract.Assert(x > 0, "because x computes as a*a + b*b");

var res = Part1.Math.Sqrt(x);

“В обычных подходах к конструированию ПО, хотя вызовы и другие операции часто основываются на корректности различных предположений, последние, чаще всего являются неявными. Разработчик уверяет себя, что некоторое свойство всегда имеет место в некоторой точке, использует этот анализ при написании кода, но после всего этого не фиксирует этого в тексте программы, в результате смысл работы теряется. Когда некто, возможно, сам автор, несколькими месяцами позже, захочет разобраться в программе, возможно, с целью ее модификации, ему придется начинать работу с нуля, поскольку все предположения остались в сознании автора. Инструкция утверждения помогает избежать подобных проблем, требуя документирования нетривиальных предположений” [Meyer2005].

ПРИМЕЧАНИЕ
В проектировании по контракту, предложенном Бертраном Мейером содержится еще один тип утверждений: инварианты и варианты циклов, которые помогают строить корректные циклы. Но поскольку этот вид утверждений большинством других реализаций принципов проектирования по контракту не поддерживается и является “тактическим”, а не “стратегическим” элементом, то в данной статье он рассматриваться не будет.

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

Введение

С момента реализации принципов проектирования по контракту в промышленном языке программирования прошло уже более десяти лет, но именно сегодня, после появления контрактов на платформе .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)

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