Uso da linguagem JML (Java Modeling Language) para a descrição de contratos de software de programas escritos na linguagem Java, de acordo com o método Design by Contract. O propósito básico de JML é especificar formalmente a interface de um método ou tipo, bem como o seu comportamento.
Para que serve:
O método Design by Contract permite que módulos de um sistema estabeleçam uma relação contratual entre si, que é caracterizada pela especificação de obrigações e benefícios. Com base nos contratos descritos, ferramentas de análise verificam se o código satisfaz o que está escrito nos contratos.
Em que situação o tema é útil:
A metodologia de Design by Contract visa à construção de sistemas mais confiáveis, reduzindo a quantidade de bugs. A linguagem JML é uma notação para especificação formal do comportamento de tipos (interfaces e classes) e métodos escritos em Java, permitindo que, por meio de verificações, possamos afirmar com mais segurança que o programa é correto, que está de acordo com sua especificação. Também registramos decisões de projeto e implementação por meio do uso de JML.
Design by Contract e Java:
O uso da linguagem JML para a especificação de tipos (classes e interfaces) e descrição do comportamento de métodos permite que verifiquemos a correção da implementação em relação à especificação dos contratos. Além disso, a especificação serve como documentação formal do software, evitando qualquer possível ambiguidade advinda de documentação em linguagem natural. A especificação formal também pode ser usada para a geração de classes de teste bem como para geração de dados de teste.
Autores: Gabriel Falconieri Freitas e Márcio Cornélio
O extenso uso de artefatos de software nos coloca diante de questões como a qualidade e a confiabilidade destes artefatos, o que influencia direta ou indiretamente a vida dos usuários. Pensando nisso, neste artigo abordaremos uma metodologia de desenvolvimento que pode auxiliar consideravelmente na melhoria da confiabilidade do software.
Vamos apresentar a técnica Design by Contract (DbC), também conhecida como Contract Programming ou Programming by Contract, e mostrar como utilizá-la no desenvolvimento de aplicações Java utilizando a linguagem JML (Java Modeling Language). Explicaremos o que são contratos e como eles podem ser úteis para prevenir erros, gerar testes unitários de forma automática, atender requisitos e gerar documentação no formato JavaDoc. Faremos isto de forma prática, demonstrando como realizar cada uma das atividades citadas utilizando softwares livres desenvolvidos pela comunidade Java e JML.
O que é DbC?
A fim de compreender como podemos usar a técnica DbC, podemos fazer uma analogia entre contratos de diversos domínios. Por exemplo, se em uma compra por comércio eletrônico, o cliente realizar o pedido até determinada hora e em certa cidade, a loja se compromete a entregar o pedido no mesmo dia. Neste caso, se o cliente atende o requisito descrito pela loja, esta se compromete com a entrega dentro do prazo definido. Podemos tomar como outro exemplo o de uma conta bancária que não seja uma conta especial. Para realizar uma operação de débito, pode-se estabelecer que o valor a ser debitado tem de ser menor ou igual ao saldo da conta (condição para a realização da operação); se isto for satisfeito, ao final, o saldo da conta será igual ao saldo imediatamente antes da realização da operação de débito subtraído do valor debitado (condição da conta após a realização da operação).
Em se tratando de DbC, a relação contratual se dá entre módulos de software. Inicialmente descrita por Bertrand Meyer tendo como alvo a linguagem Eiffel, a metodologia DbC estabelece um método de desenvolvimento de software no qual os desenvolvedores devem especificar explicitamente o que cada função de um módulo requer para ser executada de forma correta, e o que ela provê para os seus utilizadores (clientes). Estabelece-se, dessa forma, um contrato entre módulos. Os contratos são descritos por uma coleção de assertivas que descrevem precisamente o que os métodos, por exemplo, requerem para execução (pré-condição) e o que eles garantem (pós-condição) aos seus clientes após a execução. Se o cliente atende ao que é exigido na pré-condição, a pós-condição deve ser estabelecida pelo método. Assim, DbC visa à construção de sistemas orientados a objetos mais confiáveis, tendo como base os mecanismos que permitem verificar a correção de um sistema, ou seja, se a implementação está de acordo com a especificação (contrato).
De fato, o uso de pré e pós-condições no desenvolvimento de software data do final da década de 1960, o uso recente tem sido acompanhado de novas técnicas de verificação de software que permitem avaliar se o código viola o contrato descrito. Outro papel desempenhado pelos contratos é o de documentação de software, pois pode-se buscar compreender o funcionamento do código pela leitura dos contratos em vez da leitura do código. O contrato serve, então, como documentação formal, sem ambiguidade, do que o código faz.
...
