Detalhes sobre a utilização de Code Contracts

A InfoQ informou a disponibilidade do Code Contracts para .NET. Desta vez, nós queremos apresentar detalhes da utilização de Code Contracts, que são uma adição importante ao .NET.

Antes do .NET 4.0, Contratos eram adicionados aos projetos no Visual Studio ao se referenciar a biblioteca Microsoft.Contracts.dll que é instalada em %PROGRAMFILES%/Microsoft/Contracts/PublicAssemblies. O .NET 4.0 irá trazer os Contratos diretamente na biblioteca padrão mscorlib.dll. A validação através de Contratos pode ser configurada para ser executada estaticamente em tempo de compilação ou dinamicamente em tempo de execução. Há vários tipos de contratos: Pré-condições, Pós-condições, Objetos Invariantes, Asserções, Suposições, Quantificadores, Contratos de Interface e Contratos por Métodos Abstratos.

Pré-condições são definidas utilizando o método Contract.Requires() e o resultado da sua compilação aparece em Intermediate Language se o símbolo CONTRACTS_FULL ou CONTRACTS_PRECONDITIONS são usados. Um exemplo é:

Contract.Requires( x ! = null );

Esta precondição é geralmente usada para valição de parâmetros quando o programa entra no corpo de um método como no exemplo abaixo:

public Rational( int numerator, int denominator) {
   Contract.Requires( denominator ! = 0 );
   this .numerator = numerator;
   this .denominator = denominator;
}

Se a condição especificada pelo método Contract.Requires() não é atendida, então o método Debug.Assert(false) é chamado e em seguida o método Environment.FailFas(). Quando quer-se que a pré-condição esteja presente no assembly resultante, independente dos símbolos que são utilizados durante a compilação, então o método Contract.RequiresAlways() deve ser usado.

Pós-condições são contratos que devem ser atendidos quanto o método termina e são especificados pelo método Contract.Ensures() como no próximo exemplo:

public int Denominator {
  get {
     Contract.Ensures( Contract.Result() != 0 );
     return this .denominator;
  }
}

Apesar da condição ser especificada antes do return, ela é executada, na prática, após o valor de retorno ser computadol, mas antes do ponteiro de execução voltar ao método que chamou o atual.

Objetos Invariantes são condições especificadas para cada instância de uma classe:

[ContractInvariantMethod]
protected void ObjectInvariant () {
   Contract. Invariant ( this .denominator ! = 0 );
}

Outros tipos de contratos são asserções (do método Contract.Assert()) e suposições (do método Contract.Assume()). Um Assert() que falha chamará o Debug.Assert(false). Já suposições são similares às asserções em tempo de execução, mas diferem durante a verificação estática. Suposições são usadas para especificar condições que deveriam ser atendidas mas que o compilador, devido às suas limitações inerentes, não consegue verificar.

Contratos de Interface são usados para especificar condições para interfaces. Eles são especificados utilizando-se classes separadas associadas às interfaces porque uma declaração de método em interface não pode ter um corpo. O mesmo é verdade para Contratos de Métodos Abstratos.

Um exemplo de uma classe que utiliza Contratos é:

Links úteis: InfoQ news on Code Contracts, Code Contracts Download (MSI), Code Contracts documentação online (PDF), Microsoft Research Code Contracts website.