Skip navigation
Use este identificador para citar ou linkar para este item: https://repositorio.ufpe.br/handle/123456789/2580
Título: ArcAngel: a Tactic Language For Refinement and its Tool Support
Autor(es): Vinicius Medeiros Oliveira, Marcel
Palavras-chave: Tatic language;ArcAngel
Data do documento: 2002
Editor: Universidade Federal de Pernambuco
Citação: Vinicius Medeiros Oliveira, Marcel; Lúcia Caneca Cavalcanti, Ana. ArcAngel: a Tactic Language For Refinement and its Tool Support. 2002. Dissertação (Mestrado). Programa de Pós-Graduação em Ciência da Computação, Universidade Federal de Pernambuco, Recife, 2002.
Resumo: 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
URI: https://repositorio.ufpe.br/handle/123456789/2580
Aparece na(s) coleção(ções):Dissertações de Mestrado - Ciência da Computação

Arquivos deste item:
Arquivo Descrição TamanhoFormato 
arquivo5124_1.pdf1,61 MBAdobe PDFVer/Abrir


Este arquivo é protegido por direitos autorais



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.