ArcAngel: a Tactic Language For Refinement and its Tool Support / ArcAngel: a Tactic Language For Refinement and its Tool Support
AUTOR(ES)
Marcel VinÃcius Medeiros Oliveira
DATA DE PUBLICAÇÃO
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.
ASSUNTO(S)
program development formal methods refinement calculus formal methods refinement calculus ciencia da computacao program development
