Combinando Test Driven Development
(TDD) com Design By Contract (DBC)
João Arthur Brunet Monteiro
Universidade Federal de Campina Grande - UFCG
Centro de Engenharia Elétrica e Informática - CEEI
Departamento de Sistemas e Computação - DSC
Roteiro
 Introdução
 Backgroud
 Test Driven Development
 Design By Contract
 Combining Formal Specifications with Test Driven Development
 Visão Geral
 Técnica Proposta
 Resultados
 Discussões
Introdução
 Combining Formal Specifications with Test Driven Development
 Design By Contract e Test Driven Development
 Trabalho relativamente recente (2004).
Por quê?
Por quê combinar as duas técnicas?
Test Driven Development
 Técnica de desenvolvimento de software baseada em testes
 Testes são desenvolvidos antes do código
 Técnica ágil
 Pequenos passos (baby steps)
 Manter a simplicidade (KISS)
Test Driven Development
 Não constitui somente uma maneira de testar. TDD é uma
técnica desenvolvida que, ao aplicada, força o programador a
pensar no design do código antes dele ser implementado.
 Passos:
 Escrever o teste
 Obter red bar
 Escrever o código mais simples que passe no teste
 Obter green bar
 Refatorar o código
Testes
 Descrevem parcialmente, através de exemplos, o
comportamento do sistema
 Usados como documentação de um programa
 Aumentam o entendimento sobre o código
 Aumentam a qualidade do código
Mas...
 Não generalizam propriedades do sistema
Design By Contract
Metodologia que se baseia na construção de contratos entre partes do software.
 Usa especificações formais para estabelecer contratos entre partes do software
 pré-condições, pós-condições e invariantes
 Especificações formais são também usadas como documentação sem fazer
referência ao código. Por isso, aumentam a reusabilidade do software e,
consequentemente, sua qualidade
 Especificações formais descrevem o comportamento do sistema de maneira
mais completa que testes o fazem
Mas...
 A tarefa de mostrar que um software está de acordo com as especificações é
geralmente muito complexa
Por quê não?
Por quê não combinar as técnicas?
Combining Formal Specifications with
Test Driven Development
 Objetivos
 Combinar especificação formal com TDD
 Não perder a agilidade de TDD
 Ganhar com as generalizações das especificações formais
Técnica Proposta
 Os testes usados para conduzir o desenvolvimento do código
também são usados para conduzir o desenvolvimento das
especificações
 Especificações generalizam os testes
 Asserções são geradas a partir das especificações afim de checar
inconsistências entre testes, código e especificações
 Três Variáveis de interesse
 Testes
 Código
 Especificações
 Manter a consistência entre as variáveis aumenta a qualidade do
código desenvolvido e da documentação uma vez que as
especificações formais não dão margem a interpretações ambíguas
Tecnologias Utilizadas
Junit
Código
+
Java
Testes
+
JML
Especificações
Tecnologias utilizadas
 Junit e Java dispensam apresentações!
 Java Model Language (JML) é uma linguagem para
formulações de pré-condições, pós-condições e invariantes
 Especificações escritas em JML são simples de entender
 JML vem com um checador de asserções em tempo de
execução
As tecnologias foram usadas para exemplificar a técnica, no
entanto, a mesma não exige tecnologias específicas!
Técnica Proposta
 Consiste em, ao estilo TDD, uma sequência de passos que se
repetem ao longo do desenvolvimento do software.
1.
2.
3.
4.
5.
Escrever o teste
Implementar o código
Refatorar o código
Generalizar os testes para especificações
Refatorar as especificações
Aplicando a técnica
 Exemplo usado: Programa que, dado um inteiro n, retorna os
números primos até n.
Passo 1: Escrever o teste
public void testZero() {
List primes Primes.primes(0);
assertTrue(primes.isEmpty());
}
Passo 2: Escrever o código
public static List primes(int n) {
return new LinkedList();
}
Passo 3: Refatorar o código
Aplicando a técnica
Passo 4: Generalizar o teste para especificações
public bahavior
requires n<=1;
ensures \result.isEmpty();
}
 Veja que o caso de n ser igual a 1 foi coberto pela
especificação, mas não pelo teste. Analisando a especificação é
possível notar que falta um teste. No entanto, a inclusão do
novo teste não irá apontar faltas no código.
Aplicando a técnica
Passo 1: Escrever o teste
public void testTwo() {
List primes = new Primes.primes(2);
assertEquals(1, primes.size());
assertTrue( primes.contains(new Integer(2)));
}
Passo 2: Escrever o código
public static List primes(int n) {
List primes = new LinkedList();
if (n==2) primes.add(new Integer(2));
return primes;
}
Aplicando a técnica
Passo 4: : Generalizar o teste para especificações
public bahavior
requires n<=1;
ensures \result.isEmpty();
also
requires n ==2;
ensures \result.size() == 1 && \result.contains(new Integer(2));
Passo 1: Escrever o teste
public void testLosts1() {
...
for (int i = 1; i<=n ; i++) {
if (isPrime(i)) assertTrue(primes.contains(new Integer(i)))
}
}
Aplicando a técnica
 Especificação da função isPrime(int i)
public bahavior
ensures
\result < = = > (n > 1 && (\forall int i; i > 1 && i < n; n % i != 0));
Passo 2: Escrever o código
public static List primes(int n) {
List primes = new LinkedList();
for (int i = 2; i <= n; i++) primes.add(new Integer(i));
return primes;
}
Aplicando a técnica
Passo 4: : Generalizar o teste para especificações
public bahavior
requires n <= 1;
ensures \result.isEmpty();
also
requires n == 2;
ensures \result.size() == 1 && \result.contains(new Integer(2));
also
requires n > 2;
ensures (\forall int i; i >= 2 && i <= n; isPrime(i) == > \result.contains(new
Integer(i)));
Aplicando a técnica
 A especificação diz que, para um dado n, a função retorna
uma lista contendo os números primos de 2 até n. Porém,
não assegura que a lista só contém os números primos de 2 a
n.
Passo 1: Escrever o teste
public void testLosts1() {
List primes = Primes.primes(1000);
...
for (Integer i : primes) {
assertTrue(isPrime(i));
assertTrue(prime <= n);
}
}
Aplicando a técnica
Passo 2 : Escrever o código ... (crivo de Eratóstenes)
Passo 3: Refatorar o código ...
Passo 4: : Generalizar o teste para especificações
Aplicando a técnica
public bahavior
requires n <= 1;
ensures \result.isEmpty();
also
requires n == 2;
ensures \result.size() == 1 && \result.contains(new Integer(2));
also
requires n > 2;
ensures (\forall int i; i >= 2 && i <= n; isPrime(i) == > \result.contains(new
Integer(i)));
also
requires n > 2;
ensure (\forall Integer i; \result.contains(i));
isPrime(i);
Aplicando a técnica
 Em TDD é argumentado que testes não devem ser
refatorados.
 Refatorar especificações tornam-as mais claras e concisas.
Passo 5: Refatorar especificações
public bahavior
ensures
(\forall int i; i >= 2 && i <= n;
isPrime(i) == > \result.contains(new Integer(i)));
&&
(\forall Integer i; \result.contains(i);
isPrime(i);
Observações
 Rodando os testes instrumentados com as asserções geradas
pelas especificações em JML, é possível garantir que a
especificação não entra em conflito com a implementação do
código
 O caso de haver números maiores que n não foi considerado.
Mas neste caso, basta adicionar na especificação que i deve ser
menor que n
Resultados
 Como resultado do processo temos um conjunto de testes,
código e especificações que assegura que o código
implementa o comportamento esperado, documentado pela
especificação
 As especificações podem ser usadas como documentação para
descrever o comportamento do programa sem fazer
referência ao código fonte
 Note que a especificação é mais simples de entender do que
os testes e o código
 O poder de abstração aumenta com o uso das especificações
Resultados
 Bugs que não eram encontrados fazendo uso de testes, são
revelados quando a técnica é usada
 O uso da técnica ajuda a aumentar o conjunto de testes
 Assim como testes, não garante a ausência de bugs
Discussão
Dúvidas?
Referências
 Hubert Baumeister. Combining Formal Specifications with
Test Driven Development. XP/Agile Universe 2004: 1-12
 Bertrand Meyer: Applying "Design by Contract, in
Computer (IEEE), vol. 25, no. 10, October 1992, pages 4051.
 BECK, K. and FOWLER, M. (2001). Planning Extreme
Programming. Addison Wesley.