Verificando a corretude de geradores automáticos de código

Detalhes bibliográficos
Ano de defesa: 2011
Autor(a) principal: SOUSA, Thiers Garretti Ramos
Orientador(a): Não Informado pela instituição
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
Tipo de acesso: Acesso aberto
Idioma: por
Instituição de defesa: Universidade Federal de Pernambuco
Programa de Pós-Graduação: Não Informado pela instituição
Departamento: Não Informado pela instituição
País: Não Informado pela instituição
Palavras-chave em Português:
Link de acesso: https://repositorio.ufpe.br/handle/123456789/2373
Resumo: Os contratos (modelos que descrevem mais detalhadamente a arquitetura e os componentes) podem ser utilizados para a construção de softwares corretos. Esta construção pode ser realizada através do (1) cálculo de refinamento, (2) refinamento da estratégia e (3) fazendo a geração automática de código. Embora (1) e (2) são soluções corretamente comprovadas, eles requerem bastante esforço. Por outro lado, (3) é uma solução mais simples para derivação do código. No entanto, esta solução não pode fornecer um código confiável em relação aos seus contratos (ao menos que se comprove que o gerador de código é correto). Este trabalho propõe uma estratégia de testes baseados em modelos para verificar se determinado gerador de código é correto. A estratégia inicia-se com JML (linguagem baseada em contrato utilizada no Java) usando como estudo de caso o JavaCard, JMLe (um gerador de código baseado em JML) e o Jartege (gerador de testes baseados em modelos). Além disso, através deste trabalho é realizado um experimento onde é investigado o número de erros encontrados no jmle variando os valores do parâmetros do Jartege no nosso estudo de caso