Contratos de código (.NET Framework)

Os contratos de código fornecem uma maneira de especificar pré-condições, pós-condições e invariantes 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. Postconditions descrevem expectativas no momento em que o método ou código de propriedade sai. Invariantes de objeto descrevem o estado esperado para uma classe que está em um bom estado.

Os contratos de código incluem classes para marcar seu código, um analisador estático para análise em tempo de compilação e um analisador de tempo de execução. 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:

• Testes aprimorados: os contratos de código fornecem verificação estática de contrato, verificação de 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 significado que não satisfazem as 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 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 de contrato. Há também folhas de estilo que podem ser usadas com Sandcastle para que as páginas de documentação geradas tenham seções de contrato.

Todas as linguagens do .NET Framework podem aproveitar imediatamente os contratos; você não precisa escrever um analisador ou compilador especial. Um suplemento do Visual Studio permite especificar o nível de análise de contrato de código a ser executado. Os analisadores podem confirmar que os contratos estão bem formados (verificação de tipo e resolução de nomes) e podem produzir uma forma compilada dos contratos em formato de linguagem intermediária comum (CIL). 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 diferentes compilações, algumas com contratos e outras sem.

Para obter ferramentas e instruções detalhadas para usar contratos de código, consulte Contratos de código no site de mercado 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 são geralmente usados para especificar valores de parâmetros válidos. Todos os membros mencionados nas condições prévias devem ser, pelo menos, tão acessíveis como 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 tempo de execução de pré-condições com falha é 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 seu código deve lançar uma exceção específica na falha de uma pré-condição, você pode usar a sobrecarga genérica da Requires seguinte maneira.

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

Legado requer declarações

A maioria do código contém alguma validação de parâmetro na forma de if--thenthrow código. As ferramentas contratuais reconhecem estas declarações como pré-condições nos seguintes casos:

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

• Todo o conjunto de tais instruções é seguido por uma chamada de método explícitaContract, como uma chamada para o RequiresEnsures, , EnsuresOnThrow, ou EndContractBlock método.

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

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: deve ser escrita como mostrado no exemplo anterior; ou seja, não else deve conter cláusulas, e o corpo da then cláusula deve ser uma única throw declaração. O if teste está sujeito a regras de pureza e visibilidade (consulte Diretrizes de uso), mas a throw expressão está sujeita apenas a regras de pureza. No entanto, o tipo de exceção lançada deve ser tão visível quanto o método em que o contrato ocorre.

Pós-condições

As pós-condições são contratos para o estado de um método quando este termina. A pós-condição é verificada imediatamente antes de sair de um método. O comportamento em tempo de execução de pós-condições com falha é determinado pelo analisador de tempo de execução.

Ao contrário das pré-condições, as pós-condições podem fazer referência a membros com menor visibilidade. Um cliente pode não ser capaz de entender ou fazer uso de 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

Você pode expressar pós-condições padrão usando o Ensures método. 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 excecionais

Pós-condições excecionais são pós-condições que devem ser true quando uma determinada exceção é lançada 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 é lançada T .

Existem alguns tipos de exceção que são difíceis de usar em uma pós-condição excecional. Por exemplo, usar o tipo Exception for T requer que o método garanta a condição independentemente do tipo de exceção lançada, mesmo que seja um estouro de pilha ou outra exceção impossível de controlar. Você deve usar condições de postagem excecionais apenas para exceções específicas que podem ser lançadas quando um membro é chamado, por exemplo, quando um InvalidTimeZoneException é lançado para uma TimeZoneInfo chamada de método.

Pós-condições especiais

Os seguintes métodos só podem ser utilizados em condições posteriores:

• Você pode fazer referência aos valores de retorno do método em postconditions usando a expressão Contract.Result<T>(), onde T é substituído pelo tipo de retorno do método. Quando o compilador é incapaz de inferir o tipo, você deve fornecê-lo explicitamente. Por exemplo, o compilador C# é incapaz de inferir tipos para métodos que não usam nenhum argumento, portanto, ele requer a seguinte pós-condição: Contract.Ensures(0 <Contract.Result<int>()) Métodos com um tipo de retorno de void não podem se referir em Contract.Result<T>() 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 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 for capaz de inferir seu tipo. (Por exemplo, o compilador C# sempre infere o tipo porque usa um argumento.) Existem 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 ainda, uma expressão antiga deve referir-se 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 de retorno 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 ligada de um quantificador se o intervalo do quantificador depender do valor de retorno 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 delegado anônimo em uma ForAll chamada 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 pode 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 ForAll método ou Exists :

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

  • Out Os parâmetros apresentam um problema porque os contratos aparecem antes do corpo do método, e a maioria dos compiladores não permite referências a out parâmetros 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;
    }
    

    Como com o OldValue método, você pode omitir o parâmetro de tipo genérico sempre que o compilador é capaz de inferir seu tipo. O regravador de contrato substitui a chamada de método pelo valor do out parâmetro. O ValueAtReturn método pode aparecer apenas 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 . Este último também é útil quando se refere a campos na pós-condição de um construtor de estrutura.

    Nota

    Atualmente, as ferramentas de análise de contrato de código não verificam se out os parâmetros 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 tivesse usado o valor de x em vez de atribuir um inteiro a ela, um compilador não emitiria o erro correto. No entanto, em uma compilação onde o símbolo de pré-processador CONTRACTS_FULL não está definido (como uma compilação de versão), o compilador emitirá um erro.

Invariantes

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

Os métodos invariantes são identificados por serem marcados com o ContractInvariantMethodAttribute atributo. Os métodos invariantes 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 invariante individual, como mostrado no exemplo a seguir.

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

Os invariantes são definidos condicionalmente pelo símbolo CONTRACTS_FULL pré-processador. Durante a verificação em tempo de execução, os invariantes são verificados no final de cada método público. Se um invariante mencionar um método público na mesma classe, a verificação invariante que normalmente aconteceria no final desse método público será desabilitada. Em vez disso, a verificação ocorre somente no final da chamada de método mais externa para essa classe. Isso também acontece se a classe for reinserida devido a uma chamada para um método em outra classe. Invariantes não são verificados para um finalizador de objeto e uma IDisposable.Dispose implementação.

Diretrizes de uso

Encomenda de Contratos

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

Pureza

Todos os métodos que são chamados dentro de um contrato devem ser puros; ou seja, não devem atualizar nenhum estado preexistente. 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 PureAttributearquivo .

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

• Propriedade obter acessórios.

• 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 vazio).

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

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

Visibility

Todos os membros mencionados num contrato devem ser pelo menos tão visíveis como o método em que aparecem. Por exemplo, um campo privado não pode ser mencionado numa condição prévia para um método público; Os clientes não podem validar tal contrato antes de chamarem o método. No entanto, se o campo estiver marcado com o ContractPublicPropertyNameAttribute, está isento destas 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