Linguagem de especificação leve Hoare-separação para java


Autoria(s): Santos, Tiago Vieira Correia dos
Contribuinte(s)

Caires, Luís

Data(s)

28/01/2011

28/01/2011

2010

Resumo

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Esta tese tem como objectivo o desenvolvimento de uma linguagem de especificação leve para Java, e sua integração no processo de compilação. Este trabalho pretende assim, aproximar a verificação efectuada pelos sistemas de tipos de verificações lógicas mais informativas, através do uso de especificações leves em lógica proposicional. O processo de verificação é modular e baseado no cálculo de pré-condições mais fracas de Dijkstra, estendido para a linguagem orientada a objectos Java. Um aspecto distinto da nossa abordagem consiste numa técnica para lidar com aliasing, através da separação de propriedades puras de lineares, numa formulação em lógica de separação dual. Nas últimas décadas, os temas da especificação, verificação e validação de software têm vindo a apresentar um papel muito importante no seu desenvolvimento,uma vez que garantem a sua correcção e ausência de erros de execução de forma estática, reduzindo custos de manutenção e desenvolvimento. O ano passado marcou o quadragésimo aniversário do artigo An Axiomatic Basis for Computer Programming de C.A.R. Hoare, que contribuiu para a revolução deste tema. Recentemente, o uso de métodos formais para verificar propriedades de programas tem assistido a um impulso, com ferramentas e linguagens de programação (e.g. ESC/Java2, JACK, Spec#) que têm um grande poder expressivo e permitem a verificação estática de programas. Contudo, a sua maioria requer a interacção do utilizador e têm linguagens de especificação muito complexas, que são obstáculos à sua utilização. Por outro lado, as linguagens de especificação leves, apesar de apresentarem menor expressividade, permitem ainda assim raciocinar sobre propriedades interessantes de um sistema, tornando o seu uso apelativo no desenvolvimento de software. Este trabalho pretende assim contribuir com um estudo inicial do uso de especificações leves,para provar a correcção de programas orientados a objectos de uma forma mais simples e intuitiva.

Identificador

http://hdl.handle.net/10362/5016

Idioma(s)

por

Publicador

Faculdade de Ciências e Tecnologia

Direitos

openAccess

Palavras-Chave #Especificações leves #Análise estática #Compilador verificador #Lógica de Hoare #Lógica de separação #Cálculo de pré-condições mais fracas
Tipo

masterThesis