Curso de Design by Contract com JML
From Grupo de Metodos Formais
Este curso foi apresentado no JAI'05 em São Leopoldo, RS.
Autores
Resumo
Design by Contract (DBC) é um método de implementação que visa a construção de sistemas OO mais confiáveis, na medida em que provê mecanismos para detecção de violações da sua especificação. A principal idéia de DBC é que entre as classes e seus clientes seja estabelecido explicitamente um contrato. Nele, o cliente deve garantir certas condições antes de invocar os métodos da classe (pré-condições), que por sua vez deve garantir algumas propriedades após ter sido executado (pós-condições). JML (Java Modeling Language) é uma linguagem formal de especificação comportamental para Java que contém as notações essenciais de DBC como seu subconjunto. Neste minicurso os conceitos de DBC são abordados com ênfase em como utilizar JML para anotar no código o design detalhado de classes e interfaces Java. Exemplos de utilização desse método são introduzidos através do uso de algumas ferramentas.
