| dc.description | Leis de programação são importantes tanto para definir a semântica axiomática de linguagens
de programação quanto para auxiliar o processo de desenvolvimento de software.
De fato, estas leis podem ser utilizadas como base para práticas informais de desenvolvimento
como refactoring, que vem sendo popularizada por metodologias modernas, em
especial por Extreme Programming.
Embora não tenham sido suficientemente exploradas ainda, as leis de modelagem
provavelmente podem trazer benefícios similares, mas com um impacto positivo maior
em confiabilidade e produtividade, devido ao melhor suporte antecipado no processo de
desenvolvimento de software.
Em geral, transformação de modelos que preservam semântica são propostas de
maneira ad hoc tendo em vista que são difíceis de serem provadas que são consistentes
com respeito a semântica formal. Como consequência, pequenos equívocos podem levar
a transformações que deixem o modelo inconsistente.
Por estes motivos, este trabalho propõe um conjunto de leis de modelagem (que podem
ser vistas como transformações de modelos bidirecionais que preservam semântica)
que podem ser utilizas com segurança para se derivar leis mais complexas. Estas leis
descrevem transformações de modelos em Alloy, uma linguagem formal para modelagem
orientada a objetos. Além disso, será mostrada como estas leis podem ser utilizadas para
refatorar especificações em Alloy. Com o intuito de se verificar a consistência das leis,
foi proposta uma semântica denotacional para Alloy, utilizando a própria linguagem e
uma noção de equivalência indicando quando dois modelos em Alloy possuem a mesma
semântica. Por fim, o Alloy Analyzer, ferramenta utilizada para fazer análises em modelos
em Alloy, foi estendida com algumas das leis básicas propostas. Como resultado,
algumas diretrizes para a implementação de sistemas de transformação foram propostas | |
