JCIRCUS++: Uma Versão do Aplicativo JCIRCUS com uma Estratégia de Tradução de CIRCUS para Java mais Robusta
Métodos Formais, Circus, Java, Tradução
Circus é uma linguagem formal cuja sintaxe é baseada nas sintaxes das linguagens Z e CSP, e que engloba um cálculo de refinamento e comandos guardados de Dijkstra. Circus possui um parser em Java que foi desenvolvido estendendo-se o parser de Z, pela CZT (Community Z Tools). Este parser foi utilizado para a implementação de dois aplicativos Java, chamados JCircus e CRefine. CRefine é uma ferramenta que realiza o refinamento de especificações Circus. Circus possui uma estratégia de tradução de especificações Circus para Java associada a ela. Esta estratégia de tradução foi implementada e verificada através de JCircus, que foi implementado com o uso da versão mais antiga do parser de CZT. O código Java gerado por JCircus faz uso de uma API de Java chamada JCSP, que implementa uma parte das primitivas da linguagem CSP. O fato de JCSP não implementar CSP completamente faz com que a estratégia de tradução de Circus para Java seja não-trivial. Algumas primitivas de CSP, como paralelismo, escolhas externa e interna, abstração, comunicação, e multi-sincronização são implementadas em JCSP de forma parcial, ou não são implementadas. Esta qualificação tem como objetivo não apenas migrar JCircus à versão mais nova do parser de CZT, como também de: prover uma estratégia de tradução para as primitivas de CSP cuja tradução para Java não é trivial, desenvolver uma ferramenta para fazer testes de unidade com os programas gerados por JCircus, chamada JCSPUnit, e prover uma proposta de dissertação com um cronograma de atividades.