A Refinement Theory for Alloy

Detalhes bibliográficos
Ano de defesa: 2007
Autor(a) principal: Gheyi, Rohit
Orientador(a): Henrique Monteiro Borba, Paulo
Banca de defesa: Não Informado pela instituição
Tipo de documento: Tese
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/2023
Resumo: Refatoramentos são geralmente propostos de maneira ad hoc, porque é difíıcil provar formalmente que eles preservam comportamento. Na prática, desenvolvedores, mesmo utilizando ferramentas de refatoramento, têm que usar compilação e testes para garantir que os refatoramentos são corretos. Esse cenário não é desejado principalmente no desenvolvimento de sistemas críticos. No caso de refatoramento de modelos de objetos, boa parte das transformações se baseia em argumentações informais. Um outro problema é que as noções de equivalência para modelos de objetos são muito concretas, no sentido que elas assumem que os modelos devem possuir operações, ou os mesmos nomes e estruturas. Isso não é adequado em várias situações: durante refatoramento de modelos, quando usamos elementos do modelo que são auxiliares, ou quando os modelos comparados possuem elementos distintos, mas que são relacionados. Neste trabalho, nosso objetivo é propor um conjunto de transformações que preservam semântica para Alloy, que é uma linguagem formal de modelagem orientada a objetos. Nós especificamos em PVS um conjunto de regras de boa formação e estendemos a semântica para Alloy, e mostramos que as transformações propostas são corretas no provador de teoremas de PVS. Mostramos também que este conjunto de transformações ´e relativamente completo no sentido que, com ele, podemos derivar um conjunto representativo de transformações. Além disso, propomos uma noção de refinamentos mais abstrata e flexível para modelos de objetos, na qual nosso conjunto de transformações se baseia. Esta noção foi especificada em PVS, onde provamos algumas propriedades da mesma. Além de provarmos que ela é composicional, relacionamos a mesma com a noção de refinamento de dados para Z. Estas transformações são úteis não só para derivarmos refatoramentos formalmente, como também para otimizações. Além disso, mostramos que as transformações podem ser utilizadas para derivar refatoramentos que introduzem formalmente padrões de projeto em Alloy