ArcAngel: a Tactic Language For Refinement and its Tool Support

Abstract

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