A refinement theory for alloy / A refinement theory for alloy

AUTOR(ES)
DATA DE PUBLICAÇÃO

2007

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 à 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Âem 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

ASSUNTO(S)

ciencia da computacao object models prova de teoremas refinamentos refatoramentos refinements theorem proving modelos de objetos refactorings

ACESSO AO ARTIGO

Documentos Relacionados