Linguagem Imperativa 2 com
Design by Contract
Alunos: Bruno Moreno <[email protected]>
José Elias Queiroga <[email protected]>
Yuri Malheiros <[email protected]>
Samara Martins <[email protected]>
Prof.: Augusto Sampaio
1
Roteiro
 O que é DbC
 Linguagens com DbC
 Exemplo de Uso
 Linguagem imperativa 2 com DbC
 BNF
 Código com DbC
2
Introdução ao DbC
Design by Contract (DbC) ou
Programming by Contract
Criado por Bertand Meyer
implementado no Eiffel.
Definição de contratos.
Hoare logic – {P}
C {Q}
3
Linguagens com DbC
 Eifeel (DbC nativo)
 Lisaac (DbC nativo)
 Nice (DbC nativo)
 PLP LI2 (DbC nativo)
 Java - JML, Contract4J, Jcontractor, C4J
 Ruby – Ruby Contract
 Python - PyDBC
 C# - Code contract
4
Exemplo com JML
pubic class DBCteste{
int var = 0;
//@ invariant var < 20;
//@ pre x > -1 && y > -1;
//@ post \result < 1000;
public static int soma(int x, int y){
int resultado = x + y;
var = resultado + 10;
return resultado;
}
}
DBCteste.soma(10, 10);
5
Linguagem Imperativa 2 - BNF
Declaracao ::= DeclaracaoVariavel
| DeclaracaoVariavelDbC
| DeclaracaoProcedimento
| DeclaracaoProcedimentoDbC
| DeclaracaoComposta
DeclaracaoVariavel ::= "var" Id "=" Expressao [DeclaracaoVariavelDbC]
DeclaracaoVariavelDbC ::= @inv Expressao
DeclaracaoComposta ::= Declaracao "," Declaracao
DeclaracaoProcedimento ::= "proc" Id "(" [ ListaDeclaracaoParametro ] ")" "{" Comando "}"
DeclaracaoProcedimentoDbC ::= @ DeclaracaoDbC DeclaracaoProcedimento
DeclaracaoDbC ::= ParametroDbC | ParametroDbC @ DeclaracaoDbC
ParametroDbC ::= pre Expressao | pos Expressao
6
Linguagem Imperativa 2
{
var x = 0,
var y = 1,
proc teste(int z){
write("The number is:");
write(z);
x := z;
y := z + 3
};
call teste(2)
}
X é sempre
será menor que
10.
Y é sempre
maior que 0,
menor que 10 e
diferente de 5;
O argumento do
procedimento tem que
ser positivo.
7
Linguagem Imperativa 2
{
var x = 0 @inv x > 0,
var y = 1 @inv (y > 0 and y <= 10) and y != 5,
@pre z > -1,
@pos x < 20
proc teste(int z){
write("The number is:");
write(z);
x := z
y := z + 3
};
call teste(2)
}
8
Questions, Please !
9