Contratos de código

  • Artigo

Os contratos de código fornecem uma maneira para especificar pré-condições, posteriores e constantes de objeto em seu código. Pré-condições são requisitos que devem ser atendidos ao inserir um método ou propriedade. Posteriores descrevem as expectativas no momento em que o código do método ou propriedade sai. Constantes do objeto descrevem o estado esperado para uma classe que está em bom estado.

Os contratos de código incluem classes para marcação de seu código, um analisador de estático para análise em tempo de compilação e um analisador de tempo de execução. As classes de 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 de estática do contrato, a verificação de tempo de execução e a geração de documentação.

  • Ferramentas de teste automáticas: Você pode usar os contratos de código para gerar testes de unidade mais significativos, filtrando os argumentos de teste sem sentido que não satisfaçam pré-condições.

  • Verificação estática: O verificador de estático pode decidir se há quaisquer violações do contrato sem executar o programa. Ele verifica contratos implícitos, tais como null cancela a referência e os limites e contratos explícitos de matriz.

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

Todos os.NET Framework idiomas podem imediatamente aproveitar dos contratos; Você não precisará escrever um analisador especial ou um compilador. Um suplemento de Visual Studio permite que você especifique o nível de análise de contrato de código para ser executada. Os analisadores podem confirmar que os contratos são bem formados (verificação de tipo e resolução de nomes) e pode produzir um formulário compilado dos contratos no formato do Microsoft intermediate language (MSIL). Criação de contratos de Visual Studio permite tirar proveito do padrão IntelliSense fornecidas pela ferramenta.

A maioria dos métodos na classe contrato são compilados condicionalmente; ou seja, o compilador emite chamadas para esses métodos somente quando você definir um símbolo especial, cheio de CONTRATOS, usando o #define diretiva. TOTAL de CONTRATOS permite gravar contratos em seu código sem usar #ifdef diretivas; Você pode produzir compilações diferentes, alguns com contratos e outras sem.

Para as ferramentas e instruções detalhadas para usar o código de contratos, consulte Código contratos no site do MSDN DevLabs.

Pré-condições

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

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

Contract.Requires( x != null );

Se seu código deve lançar uma exceção específica em caso de falha de pré-condição, você pode usar a sobrecarga genérica de Requires como segue:

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

Legacy requer instruções

Grande parte do código contém alguns validação de parâmetros 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 de quaisquer outras declarações em um método.

  • Todo o conjunto de tais declarações é seguido por um explícito Contract chamada de método, como, por exemplo, uma chamada para o Requires, Ensures, EnsuresOnThrow, ou EndContractBlock método.

Quando if–then–throw instruções aparecem neste formulário, as ferramentas a reconhecê-los como herdado de requires instruções. Se nenhum outro contrato siga a if–then–throw de seqüência, para finalizar 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 de teste anterior é uma pré-condição negada. (A pré-condição real seria x != null.) Uma pré-condição negada é altamente restrita: Ele deve ser escrito como mostrado no exemplo anterior; ou seja, ele deve conter nenhum else cláusulas e o corpo da then cláusula deve ser um único throw instrução. O if de teste está sujeito às regras de visibilidade e pureza (consulte As diretrizes de uso), mas o throw expressão está sujeito somente à pureza de regras. No entanto, o tipo da exceção lançada deve ser tão visível como o método no qual o contrato ocorre.

Posteriores

Posteriores são contratos para o estado de um método quando ele termina. A pós-condição é verificada antes de sair de um método. O comportamento de tempo de execução do posteriores com falha é determinado pelo analisador de tempo de execução.

Ao contrário das pré-condições, posteriores podem fazer referência a membros com menos visibilidade. Um cliente talvez não consiga compreender ou fazer uso de algumas das informações expressas por uma pós-condição usando um estado particular, mas isso não afeta a capacidade do cliente para usar o método corretamente.

Posteriores padrão

Você pode expressar posteriores padrão usando o Ensures método. Posteriores express uma condição que deve ser true com a rescisão normal do método.

Contract.Ensures( this .F > 0 );

Excepcionais posteriores

Excepcionais posteriores são posteriores devem ser true quando uma determinada exceção é acionada pelo método. Você pode especificar essas posteriores usando o Contract.EnsuresOnThrow o método, como o exemplo a seguir mostra.

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 é lançada.

Existem alguns tipos de exceções que são difíceis de usar em uma pós-condição excepcional. Por exemplo, usando o tipo de Exception para T exige o método para garantir a condição, independentemente do tipo de exceção que é lançada, mesmo se for um estouro de pilha ou outros exceção impossíveis de controle. Você deve usar posteriores excepcionais apenas para exceções específicas que podem ser geradas quando um membro é chamado, por exemplo, quando um InvalidTimeZoneException é lançada para um TimeZoneInfo chamada de método.

Posteriores especiais

Os seguintes métodos podem ser usados dentro de posteriores:

  • Você pode consultar valores de retorno do método no posteriores usando a expressão Contract. Result<T>(), onde T é substituído pelo tipo de retorno do método. Quando o compilador é capaz de inferir o tipo, você deve fornecê-lo explicitamente. Por exemplo, o compilador C# é não é possível inferir os tipos de métodos que não usa argumentos, isso requer a pós-condição a seguir: Contract.Ensures(0 < Contract.Result<int>())Métodos com um tipo de retorno de void não pode se referir Contract. Result<T>() em seus posteriores.

  • Um valor de prestate 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. Sempre que o compilador é capaz de inferir o seu tipo, você pode omitir o argumento de tipo genérico. (Por exemplo, o compilador C# sempre infere o tipo porque ele leva um argumento.) Existem várias restrições que podem ocorrer em e e os contextos em que uma expressão antiga pode aparecer. Uma expressão antiga não pode conter outra expressão antigo. Mais importante, uma expressão antiga deve se referir a um valor que existiam no estado de pré-condição do método. Em outras palavras, ele deve ser uma expressão que pode ser avaliada como pré-condição do método é true. Aqui estão várias instâncias 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 esse objeto é sempre não-nulo.

    • Você não pode consultar o valor de retorno do método em uma expressão antiga:

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

    • Você não pode se referir a out parâmetros em uma expressão antiga.

    • Uma expressão antiga não pode depender de variável de um quantificador acoplada se o intervalo do quantificador depende 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 é possível consultar o parâmetro do delegado anônimo em um ForAll ou Exists , a menos que ele é usado como um indexador ou um argumento para uma chamada de método de chamada:

      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 depende em qualquer um dos parâmetros do delegado anônimo, a menos que o delegado anônimo é um argumento para o ForAll ou Exists método:

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

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

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

      Como ocorre com o OldValue<T> método, você pode omitir o parâmetro de tipo genérico, sempre que o compilador é capaz de inferir o tipo. Regravador de contrato substitui a chamada do método com o valor de out parâmetro. O ValueAtReturn<T> método só pode aparecer na posteriores. O argumento para o método deve ser um out parâmetro ou um campo de uma estrutura out parâmetro. O último também é útil quando se referem aos campos da pós-condição de um construtor de estrutura.

      Observação

    Atualmente, as ferramentas de análise do contrato de código não verificam se out parâmetros são inicializados corretamente e desconsidere seu menção no 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 número inteiro, um compilador não seria emitir corretos erro.No entanto, em uma compilação de onde o símbolo do pré-processador CONTRATOS completo não está definido (comouma versão de compilação), o compilador emitirá um erro.

Constantes

Constantes 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 sob as quais o objeto é considerado correto.

Os métodos invariável são identificados por serem marcadas com o ContractInvariantMethodAttribute atributo. Os métodos invariável não devem conter nenhum código, exceto para uma seqüência de chamadas para o Invariant método, cada qual especifica uma constante individual, conforme mostrado no exemplo a seguir.

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

Constantes condicionalmente são definidos pelo símbolo pré-processador CONTRATOS completo. Durante a verificação de tempo de execução, constantes são verificadas no final de cada método público. Se constante menciona um método público na mesma classe, a verificação de invariável normalmente aconteceria no final desse método público está desabilitada. Em vez disso, a verificação ocorre apenas no final da chamada de método externo a essa classe. Isso também acontece se a classe é reinserida por causa de uma chamada para um método de outra classe. Constantes não são verificados para finalizers objeto ou de quaisquer métodos que implementam o Dispose método.

Diretrizes de uso

Contrato de pedidos

A tabela a seguir mostra a ordem dos elementos que você deve usar quando você escreve um método de contratos.

If-then-throw statements

Pré-condições de compatibilidade públicas

Requires

Todas as pré-condições de públicas.

Ensures

Todos os públicos posteriores (normais).

EnsuresOnThrow

Todos os públicos posteriores excepcionais.

Ensures

Todos os posteriores interno/private (normais).

EnsuresOnThrow

Todos os posteriores excepcionais interno/particular.

EndContractBlock

Se o uso de if–then–throw pré-condições de estilo sem quaisquer outros contratos, fazer uma chamada para EndContractBlock para indicar que todas as anteriores, se as verificações são pré-condições.

Pureza

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

Ferramentas de contrato de código atualmente pressupõem que os elementos de código a seguir são puros:

  • Os métodos são marcados com o PureAttribute.

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

  • Assessores da propriedade get.

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

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

  • Qualquer chamada delegado, desde que o tipo de delegado é atribuído com o PureAttribute. Os tipos de delegado System.Predicate<T> e System.Comparison<T> são considerados puro.

Visibilidade

Todos os membros mencionados em um contrato devem ser pelo menos tão visíveis como o método em que aparecem. Por exemplo, um campo particular 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 que eles chamam o método. No entanto, se o campo estiver marcado com o ContractPublicPropertyNameAttribute, está isento dessas regras.

Exemplo

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

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