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

Утверждения

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

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

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