Vinicius Quaiato

Code Contracts: criando software verificável em .Net

28/06/2010

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

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:

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:

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 ArgumentExceptio_n? Repare na imagem abaixo:

Veja que o compilador nos alerta que um contrato foi violado. Isto não pode ser feito com ifs.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:

Haverá uma falha pois dissemos que quando o método terminasse de executar a propriedade TotalComDesconto deveria ser maior que 0.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:

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.

Voltar