Made available in DSpace on 2014-06-12T15:53:55Z (GMT). No. of bitstreams: 2 arquivo6386_1.pdf: 3378493 bytes, checksum: 2ea65399678659e12b1393a14ebbb799 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2007 / 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