Made available in DSpace on 2014-06-12T15:59:26Z (GMT). No. of bitstreams: 2
arquivo5124_1.pdf: 1648397 bytes, checksum: 1b326915f0743635471f1119346ed769 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2002 / O cálculo de refinamentos é uma técnica moderna para o desenvolvimento e implementa
ção de programas de uma maneira precisa, completa e consistente. A partir
de uma especificação formal, nós produzimos um programa que implementa corretamente
a especificação através de repetidas aplicações de regras de transformação,
também chamadas de leis de refinamento. Entretanto, o uso do cálculo de refinamentos
pode ser uma tarefa difícil, pois o desenvolvimento de programas pode vir
a ser longo e repetitivo.
Estratégias de desenvolvimento são refletidas em sequências de aplicações de leis
que são aplicadas repetidamente em desenvolvimentos distintos, ou até mesmo, em
pontos diferentes de um mesmo desenvolvimento. A identificação destas táticas de
desenvolvimento, documentação, e uso das mesmas em desenvolvimentos de programas
como uma simples regra de transformação trazem um grande ganho de tempo
e esforço.
Neste trabalho nós apresentamos ArcAngel, uma linguagem para definição de
táticas de refinamento baseada em Angel, e formalizamos a sua semântica. Angel é
uma linguagem de táticas de propósito geral que assume apenas que regras transformam
objetivos de prova. A semântica de ArcAngel é similar a de Angel, mas
é elaborada de maneira a levar em consideração as particularidades do cálculo de
refinamentos.
A maioria das leis algébricas de Angel não são provadas. Neste trabalho, nós apresentamos
suas provas baseadas na semântica de ArcAngel. Também apresentamos
neste trabalho uma forma normal; ela é similar àquela apresentada para táticas em
Angel. Neste respeito, nossa contribuição é dar mais detalhes nas provas de lemas
e teoremas envolvidos na estratégia de redução para esta forma normal.
Os construtores de ArcAngel são similares aos de Angel, mas são adaptados para
tratar com leis de refinamento e programas. Além disso, ArcAngel provê combinadores
estruturais que são apropriados para aplicar leis de refinamento a componentes
de programas. Usando ArcAngel, nós definimos táticas de refinamento que
refletem estratégias comuns de desenvolvimento de programas.
Finalmente, nós apresentamos Gabriel, um suporte ferramental para ArcAngel.
Gabriel trabalha como um componente de Refine, uma ferramenta que semiautomatiza
transformações de espeficações formais para programas corretos através
de sucessivas aplicaçães de leis de refinamento. Gabriel permite aos seus usuários
criar táticas e usá-las em desenvolvimento de programas
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/2580 |
| Date | January 2002 |
| Creators | Vinicius Medeiros Oliveira, Marcel |
| Contributors | Lúcia Caneca Cavalcanti, Ana |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0017 seconds