Gas hydrate growth

Os programas que comp˜oem o n´ucleo funcional do plugin BSmart ser˜ao apresentados a seguir. Destes, o type checker B e o gerador de c´odigo s˜ao parte da ferramenta acadˆemica

open-source JBtools[VOISINET, 2002; TATIBOU ¨ET et al., 2003]. O gerador de c´odigo foi estendido no presente trabalho para permitir a gerac¸˜ao de c´odigo para Java Card. Os demais programas foram implementados no intuito de fornecer apoio adicional ao m´etodo BSmart.

5.2.1

Type checker B

O parse e a verificac¸˜ao de tipagem de um m´odulo B s˜ao feitos pela ferramenta type checker. Esta ferramenta obedece a gram´atica cl´assica da notac¸˜ao B, como descrito em [ABRIAL, 1996]. Quando o parse e a verificac¸˜ao de tipagem em um arquivo contendo um m´odulo B s˜ao conclu´ıdos de forma bem sucedida, s˜ao gerados novos arquivos contendo uma representac¸˜ao intermedi´aria em XML correspondente a este m´odulo e a todos os outros que ele referencia. Dessa forma, cada elemento sint´atico de um m´odulo B ´e traduzido em uma ˆancora XML, como pode ser visto na figura 5.2.

INVARIANT balance : SHORT <Invariant> <In> <BIdentifier> balance </BIdentifier> <Set> <IntegerSet> SHORT </IntegerSet> </Set> </In> <Invariant>

Figura 5.2: Trecho de XML gerado ap´os parser/type checker de um m´odulo B

Para que seja poss´ıvel a manipulac¸˜ao dos elementos do arquivo XML gerado, a ferramenta

JBToolsfornece uma biblioteca de classes denominada B Object Library (BOL), que se constitui pela definic¸˜ao de uma classe Java para cada tag que pode ser encontrada no arquivo XML.

Por meio da BOL pode-se gerar uma representac¸˜ao sint´atica do XML como uma ´arvore de objetos Java. As demais ferramentas descritas na presente sec¸˜ao utilizam-se da ´arvore de objetos gerada para manipular de alguma forma um m´odulo B. Para tanto, cada classe da BOL fornece m´etodos set e get, bem como m´etodos para construir a representac¸˜ao textual da classe correspondente com a sintaxe da notac¸˜ao B. Essa representac¸˜ao pode ser, por exemplo, um novo m´odulo B ou uma classe Java Card, quando da gerac¸˜ao de c´odigo.

checkeroriginal. Os mais importantes foram:

• N˜ao era poss´ıvel a gerac¸˜ao de c´odigo a partir de uma implementac¸˜ao que n˜ao tinha a cl´ausula OPERATIONS.

• O type checker de uma implementac¸˜ao falhava quando esta implementava um refinamento e ambos os m´odulos viam (cl´ausula SEES) uma mesma m´aquina.

5.2.2

Analisador de conformidade B-Java Card

Devido ao hardware limitado de um smart card s˜ao impostas algumas restric¸˜oes quanto `a API e `a m´aquina virtual Java para Java Card. Por exemplo, os tipos primitivos de ponto flutuante (float e double) de Java n˜ao s˜ao implementados, h´a limitac¸˜ao quanto ao n´umero de atributos em uma classe, n˜ao h´a classe String, a implementac¸˜ao do tipo int pelo fabricante do cart˜ao ´e opcional, dentre outras.

Diante dessas restric¸˜oes, ´e necess´ario que haja uma ferramenta que analise um m´odulo B para determinar se a partir dele ´e poss´ıvel a gerac¸˜ao de classes Java Card. Na vers˜ao atual, a ferramenta de verificac¸˜ao de conformidade de um m´odulo B para Java Card verifica apenas se a tipagem das entidades (vari´aveis, parˆametros, constantes, etc.) inteiras foi feita utilizando-se um dos tipos inteiros Java Card (byte ou short).

Para esta ferramenta, ainda devem ser feitas todas as verificac¸˜oes de conformidade que sejam poss´ıveis a partir de um modulo B. De acordo com as restric¸˜oes observadas para classes e m´etodos contidas na especificac¸˜ao da m´aquina virtual Java Card [SUN MICROSYSTEMS, 2006], essas verificac¸˜oes incluem:

• Um m´odulo B n˜ao pode conter mais de 255 vari´aveis e constantes declaradas, incluindo as vari´aveis que s˜ao utilizadas e est˜ao declaradas em outros m´odulos.

• Um m´odulo B n˜ao pode conter mais que 255 operac¸˜oes que sejam traduzidas para Java

Card como m´etodos p´ublicos ou protegidos.

• O n´umero m´aximo de vari´aveis que pode ser utilizadas em uma operac¸˜ao ´e de 255, in- cluindo vari´aveis locais e parˆametros.

5.2.3

Gerador de m´odulos Java Card

O gerador de m´odulos Java Card fornece suporte para a criac¸˜ao automatizada dos m´odulos B que servir˜ao de base para a gerac¸˜ao de c´odigo Java Card. Como entrada para esta ferramenta deve ser fornecido uma m´aquina ou refinamento B e o resultado da sua execuc¸˜ao ´e a criac¸˜ao de:

• Uma m´aquina <specification name>Conversions que ser´a a base para a criac¸˜ao das cons- tantes que identificam unicamente cada operac¸˜ao e cada excec¸˜ao definida na classe applet. • Um refinamento do m´odulo recebido como entrada contendo uma vers˜ao full function das

operac¸˜oes que recebem entrada de dados, do modo como foi descrito na sec¸˜ao 4.1.3. • Uma implementac¸˜ao B (opcional) do refinamento full function.

A m´aquina Conversions declara dois conjuntos que s˜ao gerados automaticamente. Um deles contendo identificadores para as operac¸˜oes e o outro contendo identificadores para as excec¸˜oes da m´aquina. Os elementos desses conjuntos ser˜ao utilizados para a criac¸˜ao, no applet a ser gerado, de constantes que ser˜ao utilizadas pela aplicac¸˜ao host para que seja poss´ıvel a referˆencia a operac¸˜oes da m´aquina e o tratamento adequado de excec¸˜oes, caso alguma seja lanc¸ada pelo applet.

Com relac¸˜ao `a gerac¸˜ao do refinamento full function, o usu´ario da ferramenta pode escolher a m´aquina de excec¸˜ao que ser´a utilizada, que pode ser ISOException ou UserException; qual o estilo de substituic¸˜ao condicional ser´a gerado, negando ou n˜ao o predicado da parte IF, assim como o identificador para cada excec¸˜ao identificada.

Uma implementac¸˜ao B do refinamento full function tamb´em pode ser gerada automati- camente por meio desta ferramenta. Essa implementac¸˜ao deve servir de aux´ılio para que o usu´ario n˜ao tenha que fazˆe-la “ex nihilo” antes da efetiva gerac¸˜ao de c´odigo Java Card. No entanto, n˜ao h´a garantia de que a implementac¸˜ao gerada esteja totalmente correta, podendo ser ser necess´arios alguns ajustes pelo usu´ario para que a sua vers˜ao final fique de acordo com as restric¸˜oes impostas ao m´odulo de implementac¸˜ao.

5.2.4

Tradutor de c´odigo B para Java Card

O tradutor deve receber como entrada um m´odulo de implementac¸˜ao B e gerar o c´odigo

Java Card correspondente. Na vers˜ao atual do JBtools, o tradutor ´e capaz de gerar c´odigo para as linguagens Java e C#, sendo esta ´ultima n˜ao tratada neste trabalho. Apesar de ter sido

concebido com o prop´osito principal de otimizar a gerac¸˜ao de c´odigo B para Java, visando a utilizac¸˜ao do c´odigo gerado em smart cards, a traduc¸˜ao para o applet Java Card n˜ao ´e feita diretamente.

O desenvolvedor na ferramenta JBtools deve separar a l´ogica de neg´ocio do applet, que pode ser traduzida de B para uma classe Java, do c´odigo que implementa o applet em si, que deve ser feito manualmente pelo desenvolvedor. Sendo assim, o applet deve instanciar a classe da l´ogica de neg´ocio e fazer chamadas aos seus m´etodos sempre que alguma funcionalidade for requisitada.

´E f´acil perceber que a soluc¸˜ao adotada pelo JBtools n˜ao ´e eficiente, uma vez que ´e necess´aria a criac¸˜ao de mais de uma classe para fazer um trabalho que poderia ser feito dentro da pr´opria classe do applet. Um outro ponto fraco dessa ferramenta ´e que ela restringe a gerac¸˜ao de c´odigo para as entidades inteiras da m´aquina aos tipos int e short. O usu´ario tem que escolher um deles, antes da gerac¸˜ao ser efetivada, para que sejam tipadas todas as entidades num´ericas inteiras da classe gerada. Maiores detalhes quanto `as caracter´ısticas e ao funcionamento do tradutor do

JBtoolspodem ser obtidos em [TATIBOU ¨ET; VOISINET, 2002].

Na soluc¸˜ao proposta neste trabalho, modificou-se as ferramentas do JBtools (sec¸˜ao 5.4) para permitir um controle mais fino na traduc¸˜ao da tipagem das entidades inteiras, que agora podem ser tipadas explicitamente para um dos tipos inteiros permitidos em Java Card. Foram feitas tamb´em refatorac¸˜oes nas classes respons´aveis pela gerac¸˜ao de c´odigo na ferramenta JBtools e a extens˜ao destas classes para permitir a gerac¸˜ao de c´odigo para Java Card em suas duas vers˜oes (APDU e RMI).