| Summary: | 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
|
|---|
