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

[pt] Prova automática de teoremas consiste na prova de teoremas matemáticos por intermédio de programas de computador. Dependendo da linguagem lógica em uso, o processo de provar uma determinada fórmula pode não ser computável. Além disso, dependendo do cálculo dedutivo empregado, a busca por uma prova envolve lidar com a possibilidade de aplicação de longas sequências de axiomas e regras de inferência. Tudo isso reforça a necessidade da intervenção humana no processo de prova em sistemas denominados provadores interativos de teoremas ou assistentes de prova. Em um cenário típico, um usuário interage com a máquina de prova através de uma interface gráfica, normalmente implementada como um aplicativo desktop. Recentemente, porém, muitos aplicativos deste tipo passaram a ser oferecidos para seus usuários através da web. Esta forma de disponibilizar software evita que o usuário final se preocupe com questões de instalação e configuração e possibilita o acesso ao sistema de qualquer computador, com qualquer sistema operacional, bastando ter disponível uma conexão com a Internet. Nesta dissertação, estudamos possibilidades de uso da web como plataforma para a construção de ambientes interativos para prova de teoremas. Nossa proposta é estudar os diferentes modelos de interação entre usuário e ambientes de prova automatizados e verificar como estes modelos podem ser adaptados para a web. Como resultado, apresentamos uma ferramenta gráfica para visualização e manipulação direta de provas formais na web como uma interface alternativa entre usuários e provadores. / [en] Automatic theorem proving consists of proving mathematical theorems by means of computer programs. Depending on the logic used, the process of proving a formula is not computable. Moreover, depending of the deductive system applied to, the search for a proof can involve the application of long sequences of axioms and inference rules, reinforcing the need of human intervention in the proof process. Such systems are known as interactive theorem provers or proof assistants. In a typical scenario, the user interacts with the prover through a graphical interface, usually a desktop application. Recently, however, applications like those started to be delivered to users through the web. This way of software deployment avoids that final users have to deal with complex activities like prover installation and configuration and allows this user to access the system from different machines with a simple Internet connection. In this research we study the use of web as a platform for interactive theorem proving environments construction. Our purpose is to study some interaction models between user and automated proof environments and verify how these models can be adapted to work as a web application. As a result we show a graphical tool for visualization and direct manipulation of formal proofs on web to work as an alternative interface between user and proving machines.

[pt] Atualmente, a maioria dos programas para computadores é obtida através da WEB. Como muitas vezes a procedência são fontes desconhecidas, é preciso se certificar de que o código se comporta como o esperado. A solução ideal seria verificar o código contra uma especificação de políticas de segurança ,contudo, isso pode consumir muito tempo.Uma outra alternativa é fazer com que o próprio código prove ser seguro. O conceito de proof-carryng code (PCC)é baseado nessa idéia : um programa carrega consigo uma prova de sua conformidade com certas políticas de segurança. Ou seja ,ele carrega uma prova a respeito de propriedades do próprio código. Portanto, os mesmos métodos froamsi usados para a verificação de programs podem se utilizados para esta tecnolgia. Considerando este fato,neste trabalho é estudado como cálculo de Hoare, em método formal para realizar a verificação de programas, aplicado a códigos-fonte escritos em uma linguagem de programação imperativa, pode ser útil á tecnica de PCC. Conseqüentemente, são pesquisados métodos para a geração de provas de correção de programas utilizando o método citado, para tornar possível a geração de provas de segurança para PCC utilizando o cálculo de Hoare. / [en] Nowdays most computer programs are obtained from the WEB. Since their source is usually unknown, it is necessary to be sure that the code of the program behaves as expected.The ideal solution would be verify the code against a specification of safety policies.However, this can take too much time.Another approach is making the code itself prove that it is safe. The concept os proof-carryng code (PCC) is based on this idea: a program carries a proof of its conformity with certain safety policies. That is , it carries a proof cencerning properties related to the code itself. Therefore, the same formal methods employed in formal verification of programs can be used in this tecnology. Due to this fact, in this work it is studied how Hoare logic applied to source codes written in an imperative programming language, which is a formal methods are researched to generate proofs of program correctness using the method explained, so that it can be possible to generate PCC safety programs with Hoare logic.