Basic laws of object modeling

AUTOR(ES)
DATA DE PUBLICAÇÃO

2004

RESUMO

Laws of programming are important not only to define the axiomatic semantics of programming languages but also to assist in the software development process. In fact, these laws can be used as the foundation for informal development practices, such as refactorings, widely adopted due to modern methodologies, in special Extreme Programming. Although they have not been sufficiently studied yet, modeling laws might bring similar benefits, but with a greater impact on reliability and productivity, since they are used in earlier stages of the software development process. Semantics-preserving model transformations are usually proposed in an ad hoc way because it is difficult to prove that they are sound with respect to a formal semantics. So, simple mistakes lead to incorrect transformations that might, for example, introduce inconsistencies to a model. In order to avoid that, we propose a set of simple modeling laws (which can be seen as bi-directional semantics-preserving model transformations) that can be used to safely derive more complex semantics-preserving transformations. Our laws are specific for Alloy, a formal object-oriented modeling language. We also show how those laws can be used to refactor Alloy specifications. In order to prove their soundness, we propose a denotational semantics for Alloy, using itself, and an equivalence notion stating in which conditions two Alloy models have the same meaning. Furthermore, the Alloy Analyzer, which is the tool used to make analysis in Alloy models, is extended with some of the proposed basic laws. As a result, we collect some guidelines to implement transformation systems

ASSUNTO(S)

transformaÃÃo de modelos ciencia da computacao model transformations model checking formal methods refactoring verificaÃÃo de modelos mÃtodos formais refactoring

ACESSO AO ARTIGO

Documentos Relacionados