Contratos de código (.NET Framework)

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 .NET Framework. As pré-condições são requisitos que devem ser atendidos ao inserir um método ou uma propriedade. As pós-condições descrevem as expectativas no momento em que o código do método ou da propriedade é fechado. As invariáveis de objeto descrevem o estado esperado de uma classe que está em um bom estado.

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

Os benefícios dos contratos de código incluem os seguintes:

• Testes aprimorados: os contratos de código fornecem verificação de contrato estático, verificação de runtime e geração de documentação.

• Ferramentas de teste automático: use 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á violações de contrato sem executar o programa. Ele verifica se há contratos implícitos, como desreferências nulas e limites da matriz, além de contratos explícitos.

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

Todas as linguagens do .NET Framework podem aproveitar os contratos; imediatamente: não é necessário escrever um analisador ou compilador especial. Um suplemento do Visual Studio permite especificar o nível da análise do contrato de código a ser executado. Os analisadores podem confirmar se os contratos estão bem formados (verificação de tipos e resolução de nomes) e podem produzir uma forma compilada dos contratos no formato de Common Intermediate Language (CIL). A criação de contratos no Visual Studio permite aproveitar o IntelliSense padrão fornecido pela ferramenta.

A maioria dos métodos da classe de contrato é compilada condicionalmente; ou seja, o compilador emite chamadas para esses métodos somente quando um símbolo especial, CONTRACTS_FULL, é definido usando a diretiva #define. CONTRACTS_FULL permite escrever contratos no código sem o uso de diretivas #ifdef; é possível produzir diferentes builds, alguns com contratos e outras sem eles.

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

Pré-condições

É possível expressar pré-condições usando o método Contract.Requires. As pré-condições especificam o estado quando um método é invocado. Geralmente, elas são usadas para especificar valores de parâmetro válidos. Todos os membros mencionados nas 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 em runtime de pré-condições com falha é determinado pelo analisador de runtime.

Por exemplo, a pré-condição a seguir expressa que o parâmetro x não deve ser 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, use a sobrecarga genérica de Requires, conforme mostrado a seguir.

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

Instruções Requires herdadas

A maior parte do código contém alguma validação de parâmetro na forma do código if-then-throw. 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.

• O conjunto inteiro de instruções desse tipo é seguido por uma chamada de método Contract explícita, como uma chamada ao método Requires, Ensures, EnsuresOnThrow ou EndContractBlock.

Quando as instruções if-then-throw aparecem neste formato, as ferramentas as reconhecem como instruções requires herdadas. 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 cláusulas else, e o corpo da cláusula then deve ser uma instrução throw única. O teste if está sujeito às regras de pureza e visibilidade (consulte Diretrizes de uso), mas a expressão throw está sujeita apenas às regras de pureza. No entanto, o tipo da exceção gerada deve estar tão visível quanto o método no qual ocorre o contrato.

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 em 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 nem fazer uso de algumas das informações expressas por uma pós-condição usando o estado particular, 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. É possível especificar essas pós-condições usando o método Contract.EnsuresOnThrow, 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.

Há alguns tipos de exceção que são difíceis de serem usados em uma pós-condição excepcional. Por exemplo, o uso do tipo Exception para T exige o método para garantir a condição, independentemente do tipo de exceção gerado, mesmo se ele for um excedente de pilha ou outra exceção impossível de ser controlada. 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:

• É possível se referir aos valores retornados do método nas 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 puder inferir o tipo, você deverá fornecê-lo explicitamente. Por exemplo, o compilador do C# não pode inferir tipos de métodos que não usam nenhum argumento. Portanto, ele exige a seguinte pós-condição: métodos Contract.Ensures(0 <Contract.Result<int>()) 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), em que T é o tipo de e. É possível omitir o argumento de tipo genérico sempre que o compilador pode 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 em e e os contextos nos quais uma expressão antiga pode aparecer. Uma expressão antiga não pode conter outra expressão antiga. O mais importante é que uma expressão antiga deve se referir a um valor que existia no estado de pré-condição do método. Em outras palavras, ela deve ser uma expressão que possa ser avaliada, desde que a pré-condição do método seja true. Veja a seguir várias instâncias dessa regra.

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

  • Não é possível se referir ao valor retornado do método em uma expressão antiga:

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

  • Não é possível se referir aos parâmetros out em uma expressão antiga.

  • Uma expressão antiga não poderá 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 antiga não pode se referir ao parâmetro do representante anônimo em uma chamada ForAll ou Exists, a menos que ela seja usada como um indexador ou um 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 pode ocorrer no corpo de um representante anônimo se o valor da expressão antiga depender de um dos parâmetros do representante anônimo, a menos que o representante 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 classe Contract fornece o método ValueAtReturn, que permite uma pós-condição com base em um parâmetro out.

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

    Assim como ocorre com o método OldValue, é possível omitir o parâmetro de tipo genérico sempre que o compilador pode 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 parâmetro out ou um campo de um parâmetro out de estrutura. 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 no qual o símbolo do pré-processador CONTRACTS_FULL não está definido (como o build de versão ASA), 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 o objeto está visível para um cliente. Elas expressam as condições nas quais o objeto é considerado correto.

Os métodos invariáveis são identificados sendo marcados com o atributo ContractInvariantMethodAttribute. Os métodos invariáveis não devem conter nenhum código, exceto uma sequência de chamadas ao método Invariant, cada uma delas especificando uma invariável individual, conforme mostrado no exemplo a seguir.

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

As invariáveis são definidas condicionalmente pelo símbolo do pré-processador CONTRACTS_FULL. Durante a verificação em tempo de execução, as invariáveis são verificadas ao final de cada método público. Se uma invariável mencionar um método público na mesma classe, a verificação de invariáveis que normalmente ocorre ao final do 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 ocorrerá se a classe for inserida novamente devido a uma chamada a um método em outra classe. Invariáveis 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 deve ser usada ao escrever contratos de método.

Pureza

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

Atualmente, as ferramentas de contrato de código supõ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 representante 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 aparecem. Por exemplo, um campo particular não pode ser mencionado em uma pré-condição de um método público; os clientes não podem validar um contrato desse tipo antes de chamarem o método. No entanto, se o campo estiver marcado com o ContractPublicPropertyNameAttribute, ele estará 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