Skip navigation
Please use this identifier to cite or link to this item: https://repositorio.ufpe.br/handle/123456789/2023
Title: A Refinement Theory for Alloy
Authors: Gheyi, Rohit
Keywords: Refatoramentos;Refinamentos;Modelos de objetos;Prova de teoremas
Issue Date: 2007
Publisher: Universidade Federal de Pernambuco
Citation: Gheyi, Rohit; Henrique Monteiro Borba, Paulo. A Refinement Theory for Alloy. 2007. Tese (Doutorado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2007.
Abstract: 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
URI: https://repositorio.ufpe.br/handle/123456789/2023
Appears in Collections:Teses de Doutorado - Ciência da Computação

Files in This Item:
File Description SizeFormat 
arquivo6386_1.pdf3.3 MBAdobe PDFView/Open


This item is protected by original copyright



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.