Clown: A Generic GUI API for Animating Formal Specifications
Métodos Formais, Circus, Animação
Usando métodos formais, o desenvolvedor pode aumentar a confiabilidade e correção
do software. Além disso, o desenvolvedor pode concentrar-se nos requisitos funcionais.
Mas há muita resistência em se adotar essa abordagem de desenvolvimento de software.
A razão principal é a falta de suporte ferramental adequado, útil e de fácil utilização. Os
desenvolvedores normalmente escrevem o código e o testam. Estes testes geralmente consistem em checar se as saídas estão de acordo com os requisitos. Usando métodos formais nem sempre isto é possível. Linguagens de especificação formal não possuem ferramentas como animador ou simulador e muitas vezes não há interface gráfica amigável. Por outro lado elas possuem um compilador, que gera um Sistema de Transições Rotuladas (LTS). A proposta deste trabalho é produzir uma biblioteca, escrita em Java, que fornece componentes gráficos para animar especificações formais. A biblitoteca suporta as principais operacções das linguagens formais, os principais tipos de entradas e de saídas. A idéia é facilitar o processo de animação, fornecendo componentes para uma interface gráfica genérica em um formato de biblioteca que pode ser implementado para qualquer linguagem formal, utilizando apenas o LTS como entrada. Adicionalmente uma ferramenta de visualização de traces é fornecida. Ela permite a visualização das escolhas feitas pelo usuário em um formato de árvore. A intenção é melhorar a compreensão de uma especificação, executando-a, como os desenvolvedores fazem com linguagens como Java e C.