Utilize este identificador para referenciar este registo: http://hdl.handle.net/10362/5016
Título: Linguagem de especificação leve Hoare-separação para java
Autor: Santos, Tiago Vieira Correia dos
Orientador: Caires, Luís
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
Data de Defesa: 2010
Editora: Faculdade de Ciências e Tecnologia
Resumo: 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.
Descrição: Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática
URI: http://hdl.handle.net/10362/5016
Aparece nas colecções:FCT: DI - Dissertações de Mestrado

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
Santos_2010.pdf1,03 MBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.