Contratos de código (.NET Framework)

Observação

Este artigo é específico do .NET Framework. Ele não se aplica a implementações mais recentes do .NET, incluindo o .NET 6 e versões posteriores.

Os contratos de código fornecem uma maneira de especificar pré-condições, pós-condições e invariáveis de objeto no código do .NET Framework. As pré-condições são requisitos que devem ser atendidos ao inserir um método ou propriedade. As pós-condições descrevem as expectativas no momento em que o código do método ou da propriedade é fechado. Invariáveis de objeto descrevem o estado esperado para uma classe que está em um bom estado.

Observação

Não há suporte para contratos de código no .NET 5+ (incluindo versões do .NET Core). Em vez disso, considere o uso de tipos de referência anuláveis .

Os contratos de código incluem classes para marcar seu código, um analisador estático para análise de tempo de compilação e um analisador de runtime. As classes para contratos de código podem ser encontradas no System.Diagnostics.Contracts namespace.

Os benefícios dos contratos de código incluem o seguinte:

• Teste aprimorado: os contratos de código fornecem verificação estática de contratos, verificação em tempo de execução e geração de documentação.

• Ferramentas de teste automático: você pode usar contratos de código para gerar testes de unidade mais significativos filtrando argumentos de teste sem sentido que não atendem às pré-condições.

• Verificação estática: o verificador estático pode decidir se há alguma violação de contrato sem executar o programa. Ele verifica se há contratos implícitos, como dereferências nulas e limites de matriz e contratos explícitos.

• Documentação de referência: o gerador de documentação aumenta os arquivos de documentação XML existentes com informações do contrato. Também há folhas de estilo que podem ser usadas com Sandcastle para que as páginas de documentação geradas tenham seções de contrato.

Todos os idiomas do .NET Framework podem aproveitar imediatamente os contratos; você não precisa escrever um analisador ou compilador especial. Um suplemento do Visual Studio permite que você especifique o nível de análise do contrato de código a ser executado. Os analisadores podem confirmar que os contratos são bem formados (verificação de tipos e resolução de nomes) e podem produzir uma forma compilada dos contratos no formato CIL (common intermediate language). A criação de contratos no Visual Studio permite que você aproveite o IntelliSense padrão fornecido pela ferramenta.

A maioria dos métodos na classe de contrato são compilados condicionalmente; ou seja, o compilador emite chamadas para esses métodos somente quando você define um símbolo especial, CONTRACTS_FULL, usando a #define diretiva. CONTRACTS_FULL permite que você escreva contratos em seu código sem usar #ifdef diretivas; você pode produzir builds diferentes, alguns com contratos e outros sem.

Para obter ferramentas e instruções detalhadas sobre como usar contratos de código, consulte Code Contracts no site do Marketplace do Visual Studio.

Pré-condições

Você pode expressar pré-condições usando o Contract.Requires método. As pré-condições especificam o estado quando um método é invocado. Eles geralmente são usados para especificar valores de parâmetro válidos. Todos os membros mencionados em pré-condições devem ser pelo menos tão acessíveis quanto o próprio método; caso contrário, a pré-condição pode não ser compreendida por todos os chamadores de um método. A condição não deve ter efeitos colaterais. O comportamento de tempo de execução das pré-condições que falharam é determinado pelo analisador de tempo de execução.

Por exemplo, a pré-condição a seguir expressa que o parâmetro x deve ser não nulo.

Contract.Requires(x != null);

Se o código precisar gerar uma exceção específica em caso de falha de uma pré-condição, você poderá usar a sobrecarga genérica da Requires da seguinte maneira.

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

Legado Requer Declarações

A maioria dos códigos contém alguma validação de parâmetro na forma de if-then-throw código. As ferramentas de contrato reconhecem essas instruções como pré-condições nos seguintes casos:

• As instruções aparecem antes das outras instruções em um método.

• Todo o conjunto dessas instruções é seguido por uma chamada de método explícita Contract, como uma chamada para o método Requires, Ensures, EnsuresOnThrow ou EndContractBlock.

Quando if-then-throw as instruções aparecem nesse formulário, as ferramentas as reconhecem como instruções herdadas.requires Se nenhum outro contrato seguir a sequência if-then-throw, encerre o código com o método Contract.EndContractBlock.

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

Observe que a condição no teste anterior é uma pré-condição negada. (A pré-condição real seria x != null.) Uma pré-condição negada é altamente restrita: ela deve ser escrita conforme mostrado no exemplo anterior; ou seja, não deve conter else cláusulas e o corpo da then cláusula deve ser uma única throw instrução. O if teste está sujeito a regras de puridade e visibilidade (consulte Diretrizes de Uso), mas a throw expressão está sujeita apenas a regras de puridade. No entanto, o tipo da exceção gerada deve ser tão visível quanto o método no qual o contrato ocorre.

Pós-condições

Pós-condições são contratos para o estado de um método quando ele termina. A pós-condição é verificada logo antes do fechamento de um método. O comportamento de runtime de pós-condições com falha é determinado pelo analisador de runtime.

Ao contrário das pré-condições, as pós-condições podem referenciar membros com menos visibilidade. Um cliente pode não conseguir entender ou usar algumas das informações expressas por uma pós-condição usando o estado privado, mas isso não afeta a capacidade do cliente de usar o método corretamente.

Pós-condições padrão

É possível expressar pós-condições padrão usando o método Ensures. As pós-condições expressam uma condição que deve ser true após o término normal do método.

Contract.Ensures(this.F > 0);

Pós-condições excepcionais

Pós-condições excepcionais são pós-condições que devem ser true quando uma exceção específica é gerada por um método. Você pode especificar essas pós-condições usando o Contract.EnsuresOnThrow método, como mostra o exemplo a seguir.

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

O argumento é a condição que deve ser true sempre que uma exceção que é um subtipo de T é gerada.

Existem alguns tipos de exceção que são difíceis de usar em uma condição pós-excepcional. Por exemplo, usar o tipo Exception em T requer que o método garanta a condição, independentemente do tipo de exceção que é gerada, mesmo em caso de estouro de pilha ou outra exceção impossível de controlar. Você deve usar pós-condições excepcionais somente para exceções específicas que podem ser geradas quando um membro é chamado, por exemplo, quando uma InvalidTimeZoneException é gerada para uma chamada de método TimeZoneInfo.

Pós-condições especiais

Os seguintes métodos podem ser usados apenas em pós-condições:

• Você pode consultar os valores retornados pelo método em pós-condições usando a expressão Contract.Result<T>(), em que T é substituído pelo tipo de retorno do método. Quando o compilador não consegue inferir o tipo, você deve fornecê-lo explicitamente. Por exemplo, o compilador C# não pode inferir tipos para métodos que não utilizam argumentos, portanto, requer a seguinte pós-condição: Contract.Ensures(0 <Contract.Result<int>()) métodos com um tipo de retorno void não podem se referir a Contract.Result<T>() em suas pós-condições.

• Um valor de pré-estado em uma pós-condição refere-se ao valor de uma expressão no início de um método ou uma propriedade. Ele usa a expressão Contract.OldValue<T>(e), onde T é o tipo de e. Você pode omitir o argumento de tipo genérico sempre que o compilador puder inferir seu tipo. (Por exemplo, o compilador C# sempre infere o tipo porque ele usa um argumento.) Há várias restrições sobre o que pode ocorrer e e os contextos em que uma expressão antiga pode aparecer. Uma expressão antiga não pode conter outra expressão antiga. Mais importante, uma expressão antiga deve se referir a um valor que existia no estado de pré-condição do método. Em outras palavras, deve ser uma expressão que possa ser avaliada desde que a pré-condição do método seja true. Aqui estão vários exemplos dessa regra.

  • O valor deve existir no estado de pré-condição do método. Para fazer referência a um campo em um objeto, as pré-condições devem garantir que o objeto seja sempre não nulo.

  • Não é possível fazer referência ao valor retornado do método em uma expressão antiga:

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

  • Não é possível fazer referência a out parâmetros em uma expressão antiga.

  • Uma expressão antiga não pode depender da variável associada de um quantificador se o intervalo do quantificador depender do valor retornado do método:

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

  • Uma expressão anterior não pode se referir ao parâmetro do delegado anônimo em uma chamada ForAll ou Exists, a menos que seja usada como um indexador ou argumento para uma chamada de método:

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

  • Uma expressão antiga não poderá ocorrer no corpo de um delegado anônimo se o valor da expressão antiga depender de qualquer um dos parâmetros do delegado anônimo, a menos que o delegado anônimo seja um argumento para o método ForAll ou Exists.

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

  • Os parâmetros Out apresentam um problema porque os contratos aparecem antes do corpo do método e a maioria dos compiladores não permite referências aos parâmetros out em pós-condições. Para resolver esse problema, a Contract classe fornece o ValueAtReturn método, que permite uma pós-condição com base em um out parâmetro.

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

    Assim como acontece com o OldValue método, você pode omitir o parâmetro de tipo genérico sempre que o compilador for capaz de inferir seu tipo. O reescritor de contrato substitui a chamada de método pelo valor do parâmetro out. O método ValueAtReturn pode aparecer somente em pós-condições. O argumento para o método deve ser um out parâmetro ou um campo de um parâmetro de estrutura out . Esse último também é útil ao se referir a campos na pós-condição de um construtor de estrutura.

    Observação

    Atualmente, as ferramentas de análise de contrato de código não verificam se os parâmetros out são inicializados corretamente e desconsideram sua menção na pós-condição. Portanto, no exemplo anterior, se a linha após o contrato tiver usado o valor x em vez de atribuir um inteiro a ele, um compilador não emitirá o erro correto. No entanto, em um build em que o símbolo do pré-processador CONTRACTS_FULL não está definido (como um build de versão), o compilador emitirá um erro.

Invariáveis

Invariáveis de objeto são condições que devem ser verdadeiras para cada instância de uma classe sempre que esse objeto estiver visível para um cliente. Eles expressam as condições sob as quais o objeto é considerado correto.

Os métodos invariáveis são identificados por serem marcados com o ContractInvariantMethodAttribute atributo. Os métodos invariáveis não devem conter nenhum código, exceto para uma sequência de chamadas para o Invariant método, cada um dos quais especifica um invariável individual, conforme mostrado no exemplo a seguir.

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

Invariáveis são definidos condicionalmente pelo símbolo de pré-processador CONTRACTS_FULL. Durante a verificação de runtime, os invariáveis são verificados no final de cada método público. Se um invariável mencionar um método público na mesma classe, a verificação invariável que normalmente aconteceria no final desse método público será desabilitada. Em vez disso, a verificação ocorrerá somente ao final da chamada de método externa para essa classe. Isso também acontece se a classe for inserida novamente devido a uma chamada a um método em outra classe. Invariantes não são verificadas para um finalizador de objeto e uma implementação IDisposable.Dispose.

Diretrizes de uso

Ordenação de contrato

A tabela a seguir mostra a ordem dos elementos que você deve usar ao gravar contratos de método.

If-then-throw statements	Pré-condições públicas compatíveis com versões anteriores
Requires	Todas as pré-condições públicas.
Ensures	Todas as pós-condições públicas (normais).
EnsuresOnThrow	Todas as pós-condições excepcionais públicas.
Ensures	Todas as pós-condições particulares/internas (normais).
EnsuresOnThrow	Todas as pós-condições excepcionais particulares/internas.
EndContractBlock	Se você estiver usando pré-condições de estilo if-then-throw sem nenhum outro contrato, faça uma chamada a EndContractBlock para indicar que as verificações anteriores são pré-condições.

Pureza

Todos os métodos que são chamados dentro de um contrato devem ser puros; ou seja, eles não devem atualizar nenhum estado pré-existente. Um método puro tem permissão para modificar objetos que foram criados após a entrada no método puro.

Atualmente, as ferramentas de contrato de código pressupõem que os seguintes elementos de código são puros:

• Métodos marcados com o PureAttribute.

• Tipos marcados com o PureAttribute (o atributo se aplica a todos os métodos do tipo).

• Acessadores get da propriedade.

• Operadores (métodos estáticos cujos nomes começam com "op" e que têm um ou dois parâmetros e um tipo de retorno não nulo).

• Qualquer método cujo nome totalmente qualificado começa com "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" ou "System.Type".

• Qualquer representante invocado, desde que o próprio tipo de representante seja atribuído com o PureAttribute. Os tipos de delegado System.Predicate<T> e System.Comparison<T> são considerados puros.

Visibilidade

Todos os membros mencionados em um contrato devem ser pelo menos tão visíveis quanto o método no qual eles aparecem. Por exemplo, um campo privado não pode ser mencionado em uma pré-condição para um método público; os clientes não podem validar esse contrato antes de chamarem o método. No entanto, se o campo estiver marcado com o ContractPublicPropertyNameAttribute, ele será isento dessas regras.

Exemplo

O exemplo a seguir mostra o uso de contratos de código.

#define CONTRACTS_FULL

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);
    }
}

#Const CONTRACTS_FULL = True

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


    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


    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
End Class