Deteksjon av skilt
3.1 Metode for skiltdeteksjon
O suporte de ferramentas ao BSmart é composto por um conjunto de programas (se- ção 4.6.1) implementados na linguagem C++, que possibilitam a verificação sintática e de tipos em um módulo B, a geração de refinamentos e a tradução de B para Java ou Java Card. Nas suas versões iniciais, desenvolvidas durante o mestrado do autor desta tese, a distribuição desses componentes foi efetivada na forma de plugins para a IDE Eclipse [Ecl10], escolhida devido a possibilitar o desenvolvimento ágil da interface com o usuário e a fácil distribuição das ferramentas. No entanto, na versão atual, após a reengenharia do conjunto de ferramentas, optou-se por fornecê-las como aplicações independentes, que podem ser executadas em linha de comando, ou podem ser acopladas à IDE fornecida pela ferramenta Atelier B [Cle12a].
Observa-se que, na versão inicial dos programas, utilizou-se o software JBtools [Voi02] para, através de uma biblioteca fornecida por essa ferramenta, ter acesso à árvore sintática dos elementos da especificação e realizar as transformações de código para B ou Java. Apesar de
fornecer um meio ágil de desenvolvimento, a ferramenta JBtools [Voi02] apresenta alguns pro- blemas. Dentre eles, pode-se destacar a exibição de mensagens de erro pouco esclarecedoras, o tratamento inadequado da tradução de tipos para Java Card e a compatibilidade apenas com a notação clássica da linguagem B, tal qual descrita no B-Book [Abr96].
Cumpre destacar que, ao invés de se modificar o JBtools ou criar um novo conjunto de soft- warea partir do zero, buscou-se uma outra API para a manipulação de máquinas e refinamentos B. A solução encontrada foi a API BCompiler [Cle12b], que possui funcionalidade semelhante ao JBtools, com as vantagens de ser sólida, estável e amplamente compatível com o Atelier B [Cle12a], atualmente a ferramenta de referência para desenvolvimento com o método B.
Ressalta-se que a gramática B definida pelo Atelier B inclui construções que não são supor- tadas pelo B clássico (struct e record, por exemplo) e apresenta divergências quanto à forma sintática de alguns elementos. Nesse sentido, além de eliminar os problemas apresentados pelo JBtools, a migração das ferramentas do BSmart para o BCompiler possibilita a sua integração com o ambiente de desenvolvimento fornecido pelo Atelier B. Essa abordagem, além de mais robusta que a anterior, proporciona maior agilidade e comodidade ao especificador, que possui, em uma mesma IDE, todo o ambiente necessário para o desenvolvimento Java Card com o método BSmart.
Cumpre enfatizar que o software BCompiler é utilizado em todos os componentes para ma- nipular um módulo B tendo em vista geração de código para um módulo B (caso do refinamento full function) ou para Java ou Java Card. Para tanto, antes de ser realizado o propósito de cada ferramenta, é feita a verificação sintática e de tipos do módulo fornecido como entrada através de chamadas a funções fornecidas pelo BCompiler. A resolução bem sucedida dessas verifica- ções iniciais gera a árvore de parser para o módulo, tornando possível o acesso a cada elemento desse.
4.6.1 Ferramentas e APIs Desenvolvidas
Os programas para suporte ao método encontram-se representados no diagrama de classes da figura 4.18 e são descritos a seguir. Cumpre destacar que todos eles incluem a biblioteca AMNPrinter, também desenvolvida nesta tese. Ela fornece um método para cada construção que pode ser traduzida a partir de um módulo B, possibilitando a impressão, em um arquivo de texto, do seu código em B (AMNPrinterB) ou Java (AMNPrinterJava ou AMNPrinterJavaCard).
Figura 4.18: Ferramentas de suporte ao método BSmart.
ff_gen: Geração de módulos Java Card Possibilita a criação do refinamento full function e da sua máquina de contexto, conforme descrito na seção 4.4.1. Deve-se fornecer como entrada a máquina abstrata que inicia o desenvolvimento ou um refinamento dela. Para cada restrição encontrada na pré-condição de uma operação é gerada uma constante na máquina de contexto, correspondente à exceção a ser lançada, formada por um prefixo seguido do nome da operação e de um número de sequência (por exemplo, ex_op_1, ex_op_2). Após gerado, a correção do refinamento pode ser atestada por uma ferramenta de suporte ao método B, tal qual o Atelier B, através da verificação de sintaxe, tipos e de obrigações de prova.
b2java_gen: Tradução de B para Java/Java Card Traduz um ou mais módulos de imple- mentação B em seu código Java ou Java Card correspondente. É possível gerar como saída uma classe applet Java Card, Java Card ou Java. No primeiro caso, trata-se de uma classe Java Cardque herda da classe Applet da API. As únicas intervenções do gerador são a inclusão dessa informação de herança (extends javax.framework.Applet) e de importações (import) de classes da API.
Ressalta-se que o capítulo 5 detalha a o processo de tradução das construções presentes no modelo de implementação em B para as construções equivalentes na sua classe Java Card correspondente. Para tanto, utilizou-se o formalismo ASF+SDF [BKV08] com o suporte da ferramenta Meta-Environment [ME09]. Apresentam-se também, sempre que necessário, as de- cisões de projeto que foram estabelecidas para permitir a correta geração de código.
Observa-se que, no caso da tradução para Java Card, a ferramenta verifica se os módulos de implementação satisfazem as restrições impostas pela versão 2.2.2. Tendo em vista possibilitar a correta geração de código, são verificadas as propriedades a seguir descritas na especificação Java Card[Ora11]:
• Uso do tipo inteiro (int), que até a versão Java Card 2.2.2 é de implementação opcional.
• Um módulo B pode ter no máximo 255 constantes e variáveis especificadas, incluindo aquelas declaradas em módulos vistos (cláusula sees) ou inclusos (cláusula includes).
• Um módulo B pode declarar no máximo 255 operações que sejam traduzidas em métodos públicos (public) ou protegidos (protected). Na tradução desenvolvida neste trabalho, todos os métodos de serviço da aplicação Java Card são traduzidos com visibilidade pública. A única exceção é o método construtor da classe applet, gerado com visibilidade privada (private), uma vez que ele deve ser invocado somente dentro da classe, no corpo do método init, para instanciação e registro do applet junto ao ambiente de execução.
• O número máximo de variáveis locais e parâmetros que podem ser declarados em uma operação é de 255.
• Uma classe Java Card deve declarar apenas arrays de uma dimensão. Em B, um array corresponde a uma função total mapeada de um intervalo inteiro para um conjunto ou a uma sequência (seq) sobre um dado conjunto.
host_gen: Geração da API para a aplicação cliente Utiliza a biblioteca de tradução Java (AMNPrinterJava) para gerar os componentes App_Communication e App_Proxy da API de suporte para a aplicação host. Conforme descrito na seção 4.5, os demais componentes da API, referenciados pelas duas classes geradas, não necessitam ser gerados para cada aplicação, sendo fornecidos junto à ferramenta.