Basic Laws of Object Modeling

Abstract

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