Code Contracts: criando software verificável em .Net

Code Contracts é o equivalente no .NET a Design by Contract. Infelizmente o termo Design by Contract é uma marca registrada.

por Vinicius Quaiato

Code Contracts é o equivalente no .NET a Design by Contract. Infelizmente o termo Design by Contract é uma marca registrada.

Estes contratos nos permitem escrever software de uma forma verificável, onde podemos garantir pré-condições, pós-condições e invariantes.

Me agrada a idéia também de que o código se torna mais claro e limpo. Ficam claramente expressas as inteções do código, as regras se tornam explícitas ao invés de estarem escondidas em emaranhados de condicionais.
Vamos entender então um pouco de Contratos.

Pré-condição é uma condição que deve ser satisfeita, sempre, no início da execução do método

Geralmente as pré-condições dizem respeito a verificação e garantia de valores para os parâmetros de um método. No entanto podem existir outras utilizações.

Pós-condição é uma condição que deve ser garantida ao término da execução do método

As pós-condições podem ser utilizadas para garantir que um determinado resultado seja retornado pelo método ou ainda que um determinado estado na classe tenha sido contemplado.

Invariante é uma condição que deve ser verdadeira ao longo de toda a vida de um objeto.

Invariante diz respeito a um estado que deve ser mantido durante toda a vida de um objeto, podendo por exemplo definir que o valor de um atributo da classe que não pode ter determinado valor nunca.

Vamos iniciar um novo projeto de testes.

Após criar a solution, clique com o botão direito no projeto, e vá em properties. Na tela que abrirá, selecione a aba Code Contracts e habilite os campos conforme abaixo:

Habilitando Code Contracts no projeto

Caso você não possua essa opção, faça o download e instale a ferramenta neste link (utilize a versão premium).

Após estar com o Code Contracts habilitado, vamos para a classe de testes e vamos escrever um método:

[TestMethod]
public void Deve_Realizar_Uma_Divisao()
{
    Dividir(10, 0);
}

float Dividir(float valor, float divisor)
{
    return valor / divisor;
}

Como sabemos, não podemos dividir um número por zero, desta forma vamos usar o Code Contracts para garantir isso:

1
2
3
4
5
6

float Dividir(float valor, float divisor)
{
    Contract.Requires(divisor > 0);

    return valor / divisor;
}

Podemos ver na linha 3 que estamos realizando uma chamada para o método estático Requires. É com este método que garantimos pré-condições. Ou seja, neste caso é uma pré-condição que o parâmetro divisor seja maior que 0.

Agora, qual a diferença com relação a um if(divisor < 0) throw new ArgumentException? Repare na imagem abaixo:

Verificações esdtáticas com Code Contracts

Vamos criar um método para ver como funciona a pós-condição.
Verificamos uma pós-condição utilizando o método Ensures. Para isso vou utilizar o seguinte código:

class Compra
{
    public List<Tuple<int, float>> 
QuantidadeValorProdutos = new List<Tuple<int, float>>();
    public float TotalComDesconto { get; set; }

    public void CalcularTotalComDesconto()
    {
        Contract.Requires(QuantidadeValorProdutos.Count > 0);
        Contract.Ensures(this.TotalComDesconto > 0);
    }
}

E o método de teste:

[TestMethod]
public void Deve_Calcular_Total_Da_Compra_Com_Descontos()
{
    var compra = new Compra();
    compra.QuantidadeValorProdutos.Add(new Tuple<int, float>(1,10));

    compra.CalcularTotalComDesconto();
}

E o resultado será o seguinte:

Pós-condição falhando com Code Contracts

Vamos alterar o método de cálculo para que satisfaça a pós-condição:

public void CalcularTotalComDesconto()
{
    Contract.Requires(QuantidadeValorProdutos.Count > 0);
    Contract.Ensures(this.TotalComDesconto > 0);

    this.TotalComDesconto = this.QuantidadeValorProdutos.Sum(p => p.Item1 * p.Item2);
}

Isso faz com que a propriedade TotalComDesconto receba um valor. Ainda assim essa pós-condição pode falhar. Portanto é muito importante termos consciência de como definir nossas classes e regras de negócios. Entendendo muito bem como elas devem se comportar.

E para finalizar, vamos dar uma olhada em como funcionam as invariantes.

class Usuario
{
    public string Login { get; set; }
    public string Senha { get; set; }

    public void AlterarSenhaAtual(string novaSenha)
    {
        this.Senha = novaSenha;
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(this.Senha != null);
    }
}

Uma invariante é uma condição que deve ser satisfeita ao longo de toda a vida de um objeto. Desta forma Marcamos o método com um atributo ContractInvariantMethod e dentro deste método definimos o contrato chamando o método Invariant. No exemplo acima está definido que um objeto do tipo Usuario nunca poderá ter uma senha nula.

Se executarmos o teste abaixo teremos um erro:

[TestMethod]
public void Deve_alterar_Senha()
{
    var usuario = new Ususario();
    usuario.AlterarSenhaAtual(null);
}

E o resultado:

Invariante falhando com Code Contracts

Existem outras funcionalidades presentes no Code Contracts (veja manual do usuário), e vale bastante estudá-las e entender como podem nos auxiliar.
Particularmente a clareza que temos no código, deixando bem separado o que são condicionais e o que são regras, é muito atraente pra mim.
Há a possibilidade de gerar documentação com as informações dos contratos por exemplo.

A possibilidade de checagem estática é muito válida, pois nos possibilita encontrar chamadas inválidas muito antes de que elas possam causar sérios problemas.

Enfim, é uma ferramenta e tecnologia que devemos olhar com bastante atenção.

Abraços,
Vinicius Quaiato.