Sekizinci Alt Probleme İlişkin Bulgular ve Yorumlar

Cumpre ressaltar que foi preciso criar meios para tratar as limitações do refinamento em B, tendo em vista possibilitar a verificação do modelo concreto da especificação Java Card quando

há mudança de interface em relação ao componente abstrato. No método B, não é possível modificar a interface da especificação em um refinamento posterior, mesmo que, intuitivamente, ainda haja equivalência entre os modelos abstratos e concretos. Em uma operação, isso inclui a representação dos tipos de dados, a ordem e a quantidade dos seus parâmetros de entrada e saída.

Observa-se que, em alguns casos, a mudança na interface concreta faz-se necessária, com o objetivo de compatibilizar esse modelo com as limitações de Java Card ou representar a recepção e envio de informações através do buffer adpu. Por exemplo, no caso da representação do tipo inteiro (int) de Java, uma vez que não é garantida a sua implementação em Java Card, deve-se representá-lo, no modelo concreto, como dois valores short ou como um array de bytes. É importante destacar que, no formalismo Event-B, contribuição recente derivada em parte do método B, a interface entre as operações refinadas pode ser modificada. Por outro lado, conforme discutido no capítulo 3 (seção 3.3), Event-B não é adequado ao desenvolvimento de software conforme proposto neste trabalho. Desse modo, preferiu-se continuar a utilizar o método B tradicional, buscando soluções para verificar o “refinamento” de módulos com interface distinta.

A seção 4.4.1 apresenta uma abordagem, desenvolvida nesta tese, que corresponde a uma forma de composição de módulos que resolve o problema da adaptação de interface sem a necessidade de se desviar do refinamento clássico de B. A título de ilustração, na seção 4.7, demonstra-se o uso da técnica de retrenchment [BP98], solução inicial pesquisada para contor- nar a restrição de mudança de interface. Trata-se de uma variante menos rigorosa do refinamento tradicional, e, por esse motivo, não foi incorporada ao método.

4.4.1 Um método de “refinamento” para permitir a mudança de interface

Nesta seção apresenta-se uma técnica, desenvolvida na presente tese, para permitir a ve- rificação da mudança de tipos e de interface entre um módulo abstrato e seu correspondente concreto, sem no entanto sair do escopo do método B tradicional.

Diante da impossibilidade de se verificar diretamente que a máquina Java Card (JC_App) é um refinamento da especificação Java inicial (J_App), o método proposto define um padrão de adaptação de interface a partir do refinamento do modelo abstrato. Para tanto, as operações refinadas devem manter a interface abstrata e as transições de estado em seu corpo devem ser feitas por meio das operações correspondentes do componente concreto (JC_App). Caso esse processo verifique-se correto, através da verificação das obrigações de prova do refinamento,

então é possível atestar que esses modelos são equivalentes.

O módulo J_ App_r (figura 4.11) representa o modelo a ser seguido para utilizar a técnica proposta. Para tanto, deve-se refinar a máquina abstrata Java (REFINES J_App) e incluir a especificação concreta (INCLUDES JC_App). No invariante, deve-se relacionar os estados des- ses modelos através de um invariante de ligação. No caso geral, em que a representação dos tipos concretos e abstratos é distinta, são utilizadas funções para converter o estado concreto no estado abstrato correspondente (na figura, j_v = java_of_jc ( jc_v )). Ressalta-se que deve ser fornecida, para cada tipo relacionado, uma função que faz o trabalho inverso, ou seja, que converte o estado abstrato em seu correspondente concreto (como jc_of_java (jc_param), no corpo da operação). Nesse caso, as funções são bijetoras, sendo uma inversa da outra.

REFINEMENT J_ App_r REFINES J_App

SEES J_Context, JC_Context, InterfaceContext INCLUDES JC_App

INVARIANT

j_v= java_of_jc ( jc_v ) OPERATIONS

j_r← j_operation ( j_param) = PRE j_param ∈ J_TYPE ∧

j_pre( j_param) = TRUE THEN

VAR tmp IN

tmp← jc_operation ( jc_of_java ( j_param)) ; j_r:= java_of_jc (tmp)

END END END

Figura 4.11: Refinamento da especificação abstrata inicial para verificar a correção da mudança de interface pelo módulo Java Card.

Observa-se que as operações de J_App_r possuem a mesma assinatura que o componente abstrato, dessa forma possibilitando o refinamento. A adaptação é feita no corpo da operação refinada, em um processo de três passos, para o caso de uma operação que possui parâmetros de entrada e retorno de dados:

1. Inicialmente, o valor armazenado nos parâmetros abstratos (j_param) é convertido em um valor equivalente no tipo concreto (jc_of _java(j_param));

2. Posteriormente, a operação concreta é aplicada sobre os dados concretos tmp ← jc_operation( jc_of _java(j_param));

3. Por fim, o resultado da aplicação da operação Java Card é convertido para o tipo abstrato e retornado (j_r := java_of _jc(tmp)).

As funções de conversão utilizadas para efetuar a relação de refinamento entre os estados abstratos e concretos são definidas na máquina InterfaceContext (figura 4.12). Essas funções, uma vez definidas e verificadas, podem ser reutilizadas em outros desenvolvimentos. Como tra- balhos futuros, deve-se prover uma versão do módulo InterfaceContext contendo um conjunto verificado de funções de conversão entre os tipos de dados mais comuns, por exemplo, entre tipos básicos e arrays de bytes. O módulo InterfaceContext também contém alguns corolários na cláusula ASSERTIONS que especificam propriedades adicionais para facilitar o trabalho de verificação do desenvolvimento.

MACHINE InterfaceContext SEES JInt , JCInt

CONSTANTS java_of_jc, jc_of_java PROPERTIES

java_of_jc∈ JC_TYPE ֌։ JAVA_TYPE ∧ jc_of_java∈ JAVA_TYPE ֌։ JC_TYPE ∧ jc_of_java−1_{= java_of_jc}

ASSERTIONS

java_of_jc−1= jc_of_java ∧ dom ( java_of_jc ) = JC_TYPE ∧ dom ( jc_of_java ) = JAVA_TYPE END

Figura 4.12: A máquina InterfaceContext.

Destaca-se também que, nesta proposta, uma vez que se tenha provado a equivalência dos componentes abstratos e concretos para alguma representação de tipo, obtidas através da correta verificação do refinamento J_App_r, torna-se possível reusar a abordagem para esses tipos em outros desenvolvimentos semelhantes, sem a necessidade de verificá-los novamente.

Ressalta-se que, na versão atual do método, o desenvolvimento desta etapa é feito de forma manual. Pretende-se automatizar esse processo através de uma ferramenta que gere (ao menos em parte) o padrão de refinamento proposto a partir dos modelos Java e Java Card.