Контракты для кода

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

Контракты кода содержат классы для маркировки кода, статический анализатор для анализа во время компиляции и анализатор времени выполнения. Классы для контрактов кода можно найти в пространстве имен System.Diagnostics.Contracts.

Использование контрактов кода обеспечивает следующие преимущества:

• Улучшение тестирования — контракты кода обеспечивают проверку статических контрактов, проверку во время выполнения и создание документации.

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

• Статическая проверка — средство статической проверки может обнаружить нарушения контрактов без выполнения программы. Оно проверяет неявные контракты, такие как разыменование значения NULL и границы массивов, и явные контракты.

• Справочная документация — генератор документации расширяет существующие XML-файлы документации, вставляя в них сведения о контрактах. Также существуют таблицы стилей, которые можно использовать со средством Sandcastle, чтобы сформированные страницы документации содержали разделы контрактов.

Все языки платформы .NET Framework могут немедленно воспользоваться преимуществами контрактов; писать специальное средство синтаксического разбора или компилятор не понадобится. Надстройка Visual Studio позволяет задать уровень выполняемого анализа контрактов кода. Анализаторы могут подтвердить, что контракты правильно сформированы (проверка типов и разрешение имен), и могут создать скомпилированную форму контрактов в формате языка MSIL. Разработка контрактов в Visual Studio позволяет воспользоваться преимуществом стандартной функции IntelliSense, предоставленной этим средством.

Большинство методов в классе контрактов являются условно скомпилированными, то есть компилятор выдает вызовы других методов, только если определен специальный символ, CONTRACTS FULL, используя директиву #define. CONTRACTS FULL позволяет писать контракты в коде, не используя директив #ifdef, можно создавать различные построения, некоторые с контрактами, а другие без них.

Описание средств и подробные инструкции для использования контрактов кода см. в описании Контракты кода (на английском языке) на веб-сайте MSDN DevLabs.

Предусловия

Предварительные условия можно выразить с помощью метода Contract.Requires. Предварительные условия задают состояние вызова метода. Они обычно используются, чтобы задать допустимые значения параметров. Все члены, упомянутые в предварительных условиях, должны быть по крайней мере столь же доступными, сколь и сам метод. В противном случае предварительное условие могло бы оказаться непонятым всеми объектами, вызывающими метод. У условия не должно быть побочных эффектов. Поведение невыполненных предварительных условий во время выполнения определяется анализатором времени выполнения.

Например, следующее предварительное условие показывает, что значение параметра x должно отличаться от NULL.

Contract.Requires( x != null );

Если код должен создать конкретное исключение при невыполнении предварительного условия, можно использовать следующую универсальную перегрузку метода Requires.

Contract.Requires<ArgumentNullException>( x != null, "x" );

Устаревшие операторы requires

Большая часть кода содержит определенную проверку параметров в виде кода if-then-throw. Средства контракта распознают эти операторы как предварительные условия в следующих случаях:

• Операторы в методе появляются перед всеми остальными операторами.

• Весь набор подобных операторов, за которым следует явный вызов метода Contract, например вызов метода Requires, Ensures, EnsuresOnThrow или EndContractBlock.

Когда в этой форме появляются операторы if-then-throw, средства распознают их как устаревшие операторы requires. Если после последовательности if-then-throw нет других контрактов, завершите код методом Contract.EndContractBlock.

if ( x == null ) throw new ...
Contract.EndContractBlock(); // All previous "if" checks are preconditions

Обратите внимание, что условие в предыдущем тесте является предварительным условием с отрицанием. (Фактическим предварительным условием было бы x != null.) Предварительное условие с отрицанием является сильно ограниченным: оно должно быть написано так, как показано в предыдущем примере, то есть оно не должно содержать предложения else, а предложение then должно быть единым оператором throw. Проверка if подчиняется как правилам чистоты, так и правилам видимости (см. Правила использования), а к выражению throw применяются только правила чистоты. Но видимость типа созданного исключения должна быть такой же, как у метода, в котором возникает контракт.

Постусловия

Постусловия — это контракты для состояния метода при его окончании. Постусловие проверяется непосредственно перед выходом из метода. Поведение невыполненных постусловий во время выполнения определяется анализатором времени выполнения.

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

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

Стандартные постусловия можно выразить с помощью метода Ensures. Постусловия выражают условие, которое должно принимать значение true при нормальном завершении метода.

Contract.Ensures( this .F > 0 );

Постусловия для исключений

Постусловия для исключений — это постусловия, которые должны принимать значение true, когда метод создает конкретное исключение. Эти постусловия можно задать с помощью метода Contract.EnsuresOnThrow, как показано в следующем примере.

Contract.EnsuresOnThrow<T>( this.F > 0 );

Аргумент является условием, которое должно принимать значение true при создании любого исключения, являющегося подтипом T.

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

Специальные постусловия

Следующие методы могут использоваться только в постусловиях:

• В постусловиях можно ссылаться на значения, возвращаемые методом, используя выражение Contract. Result<T>(), где вместо T подставляется тип значений, возвращаемых методом. Когда компилятор не может определить тип, необходимо предоставить его явно. Например, компилятор C# не может определить типы методов, в которые не передаются никакие аргументы, поэтому для него требуется следующее постусловие: Contract.Ensures(0 < Contract.Result<int>()) Методы с возвращаемым типом void не могут ссылаться на Contract. Result<T>() в своих постусловиях.

• Значением предварительного состояния в постусловии называется значение выражения в начале метода или свойства. Оно использует выражение Contract.OldValue<T>(e), где T — это тип e. Аргумент общего типа можно опустить каждый раз, когда компилятор способен определить его тип. (Например, компилятор C# всегда определяет этот тип, так как он получает аргумент.) Существует ряд ограничений на то, что может произойти в e, и на контексты, в которых может появиться старое выражение. Старое выражение не может содержать другое старое выражение. Самое главное, старое выражение должно ссылаться на значение, существующее в состоянии предварительного условия метода. Другими словами, оно должно быть выражением, оценка которого может быть выполнена, пока значением предварительного условия является true. Вот несколько примеров этого правила.

  • Значение должно существовать в состоянии предварительного условия метода. Чтобы ссылаться на поле объекта, предварительные условия должны гарантировать, что значение объекта всегда отличается от NULL.

  • В старом выражении нельзя ссылаться на значение, возвращаемое методом:

    Contract.OldValue(Contract.Result<int>() + x) // ERROR
    

  • В старом выражении нельзя ссылаться на параметры out.

  • Старое выражение не может зависеть от привязанной переменной квантификатора, если диапазон квантификатора зависит от возвращаемого методом значения:

    Contract. ForAll (0,Contract. Result<int>(),
    i => Contract.OldValue(xs[i]) > 3 ); // ERROR
    

  • Старое выражение не может ссылаться на параметр анонимного делегата в вызове метода ForAll или Exists, если оно используется не как индексатор или аргумент вызова метода:

    Contract. ForAll (0, xs .Length, i => Contract.OldValue(xs[i]) > 3); // OK
    Contract. ForAll (0, xs .Length, i => Contract.OldValue(i) > 3 ); // ERROR
    

  • Старое выражение не может появляться в коде анонимного делегата, если значение старого выражения зависит от каких-либо параметров анонимного делегата, кроме случаев, когда анонимный делегат является аргументом метода ForAll или Exists:

    Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
    

  • Параметры Out являются проблемой, так как контракты появляются до тела метода, и большинство компиляторов на разрешают ссылаться на параметры out в постусловиях. Для решения этой проблемы класс Contract предоставляет метод ValueAtReturn<T>, разрешающий использовать постусловие на основе параметра out.

    public void OutParam(out int x) f
    Contract.Ensures(Contract.ValueAtReturn(out x) == 3);
    x = 3;
    

    Как и в случае метода OldValue<T>, параметр общего типа можно опустить каждый раз, когда компилятор способен определить его тип. Средство перезаписи контракта заменяет вызов метода значением параметра out. Метод ValueAtReturn<T> может появляться только в постусловиях. Аргумент метода должен быть параметром out или полем параметра структуры out. Последний вариант также полезен при ссылке на поля в постусловии конструктора структуры.

    Примечание

    В настоящее время средства анализа кода контрактов не проверяют, правильно ли инициализированы параметры out, и пропускают их упоминание в постусловии.Следовательно, в предыдущем примере, если в строке после контракта вместо назначения целого значения использовалось значение x, компилятор не будет выдавать правильную ошибку.Но для построения, в котором не определен символ препроцессора CONTRACTS FULL (например, дляпостроения выпуска), компилятор выдаст ошибку.

Инварианты

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

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

[ContractInvariantMethod]
protected void ObjectInvariant () 
{
Contract.Invariant ( this.y >= 0 );
Contract.Invariant ( this.x > this.y );
...
}

Инварианты обычно определяются символом препроцессора CONTRACTS FULL. Во время проверки времени выполнения инварианты проверяются в конце каждого открытого метода. Если инвариант упоминает открытый метод в том же классе, проверка инварианта, обычно выполняемая в конце открытого метода, отключается. Вместо этого проверка выполняется только в конце вызова самого внешнего метода, обращающегося к этому классу. Она также выполняется при повторном входе в класс из-за вызова метода для другого класса. Инварианты не проверяются для методов завершения объектов или для любых методов, реализующих метод Dispose.

Правила использования

Порядок в контрактах

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

If-then-throw statements	Обратно совместимые открытые предварительные условия
Requires	Все открытые предварительные условия.
Ensures	Все открытые (обычные) постусловия.
EnsuresOnThrow	Все открытые постусловия для исключений.
Ensures	Все закрытые/внутренние (обычные) постусловия.
EnsuresOnThrow	Все закрытые/внутренние постусловия для исключений.
EndContractBlock	При использовании предварительных условий вида if-then-throw без каких-либо других контрактов поместите вызов в метод EndContractBlock, чтобы показать, что все предыдущие проверки "if" являются предварительными условиями.

Чистота

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

Средства работы с контрактами кода предполагают, что чистыми являются следующие элементы кода:

• Методы, помеченные с помощью атрибута PureAttribute.

• Типы, помеченные с помощью атрибута PureAttribute (атрибут применяется ко всем методам типа).

• Методы доступа к свойствам "get".

• Операторы (статические методы, имена которых начинаются с "op", которые обладают одним или двумя параметрами и возвращаемый тип которых отличается от "void").

• Любой метод, полное имя которого начинается с "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" или "System.Type".

• Любой вызываемый делегат при условии, что у типа этого делегата есть атрибут PureAttribute. Типы делегатов System.Predicate<T> и System.Comparison<T> считаются чистыми.

Видимость

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

Пример

В следующем примере показано использование контрактов кода.

Imports System
Imports System.Diagnostics.Contracts


' An IArray is an ordered collection of objects.    
<ContractClass(GetType(IArrayContract))> _
Public Interface IArray
    ' The Item property provides methods to read and edit entries in the array.

    Default Property Item(ByVal index As Integer) As [Object]


    ReadOnly Property Count() As Integer


    ' Adds an item to the list.  
    ' The return value is the position the new element was inserted in.
    Function Add(ByVal value As Object) As Integer

    ' Removes all items from the list.
    Sub Clear()

    ' Inserts value into the array at position index.
    ' index must be non-negative and less than or equal to the 
    ' number of elements in the array.  If index equals the number
    ' of items in the array, then value is appended to the end.
    Sub Insert(ByVal index As Integer, ByVal value As [Object])


    ' Removes the item at position index.
    Sub RemoveAt(ByVal index As Integer)
End Interface 'IArray

<ContractClassFor(GetType(IArray))> _
Friend MustInherit Class IArrayContract
    Implements IArray

    Function Add(ByVal value As Object) As Integer Implements IArray.Add
        ' Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result(Of Integer)() >= -1) '
        Contract.Ensures(Contract.Result(Of Integer)() < CType(Me, IArray).Count) '
        Return 0

    End Function 'IArray.Add

    Default Property Item(ByVal index As Integer) As Object Implements IArray.Item
        Get
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
            Return 0 '
        End Get
        Set(ByVal value As [Object])
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
        End Set
    End Property

    Public ReadOnly Property Count() As Integer Implements IArray.Count
        Get
            Contract.Requires(Count >= 0)
            Contract.Requires(Count <= CType(Me, IArray).Count)
            Return 0 '
        End Get
    End Property

    Sub Clear() Implements IArray.Clear
        Contract.Ensures(CType(Me, IArray).Count = 0)

    End Sub 'IArray.Clear


    Sub Insert(ByVal index As Integer, ByVal value As [Object]) Implements IArray.Insert
        Contract.Requires(index >= 0)
        Contract.Requires(index <= CType(Me, IArray).Count) ' For inserting immediately after the end.
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) + 1)

    End Sub 'IArray.Insert


    Sub RemoveAt(ByVal index As Integer) Implements IArray.RemoveAt
        Contract.Requires(index >= 0)
        Contract.Requires(index < CType(Me, IArray).Count)
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) - 1)

    End Sub 'IArray.RemoveAt
End Class 'IArrayContract

using System;
using System.Diagnostics.Contracts;

// An IArray is an ordered collection of objects.    
[ContractClass(typeof(IArrayContract))]
public interface IArray
{
    // The Item property provides methods to read and edit entries in the array.
    Object this[int index]
    {
        get;
        set;
    }

    int Count
    {
        get;

    }

    // Adds an item to the list.  
    // The return value is the position the new element was inserted in.
    int Add(Object value);

    // Removes all items from the list.
    void Clear();

    // Inserts value into the array at position index.
    // index must be non-negative and less than or equal to the 
    // number of elements in the array.  If index equals the number
    // of items in the array, then value is appended to the end.
    void Insert(int index, Object value);


    // Removes the item at position index.
    void RemoveAt(int index);
}

[ContractClassFor(typeof(IArray))]
internal abstract class IArrayContract : IArray
{
    int IArray.Add(Object value)
    {
        // Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result<int>() >= -1);
        Contract.Ensures(Contract.Result<int>() < ((IArray)this).Count);
        return default(int);
    }
    Object IArray.this[int index]
    {
        get
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
            return default(int);
        }
        set
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
        }
    }
    public int Count
    {
        get
        {
            Contract.Requires(Count >= 0);
            Contract.Requires(Count <= ((IArray)this).Count);
            return default(int);
        }
    }

    void IArray.Clear()
    {
        Contract.Ensures(((IArray)this).Count == 0);
    }

    void IArray.Insert(int index, Object value)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index <= ((IArray)this).Count);  // For inserting immediately after the end.
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) + 1);
    }

    void IArray.RemoveAt(int index)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index < ((IArray)this).Count);
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) - 1);
    }
}