Implementering av bakgrunnssubtraksjon

Na seção 4.4.1 descreveu-se uma técnica para possibilitar a verificação entre modelos abs- tratos e concretos com interface distinta. Através de um refinamento alternativo de adaptação de interfaces, foi possível que o método BSmart continuasse dentro do escopo de verificação com o método B.

Nesta seção apresenta-se uma solução alternativa, utilizando a teoria de retrenchment, que foi inicialmente aplicada visando contornar essa restrição de B. Uma vez que a abordagem desenvolvida na tese é mais rigorosa, por continuar na teoria de refinamento em B, preferiu-se incorporá-la ao método em detrimento ao retrenchment.

A técnica denominada retrenchment foi proposta por Banach e Poppleton [BP98], com a motivação de estender a aplicabilidade do desenvolvimento formal para uma gama maior de aplicações. O retrenchment impõe menos restrições, quando comparado ao refinamento tradicional, devido a flexibilizar a conexão entre as operações abstratas e concretas.

Ressalte-se que, utilizando-se essa técnica, pode-se especificar e verificar situações que não seriam permitidas ao refinamento. No retrenchment, é possível fortalecer a pré-condição de uma operação e/ou enfraquecer a sua pós-condição. Dessa forma, torna-se possível modificar a interface de uma operação, ou transferir parte do comportamento das variáveis de estado para variáveis de entrada e saída, ou vice-versa. Por outro lado, os mecanismos que permitem essa flexibilização, também tornam o retrenchment menos rigoroso em relação ao refinamento tradicional, conforme será discutido posteriormente nesta seção.

No artigo [BP98], os autores apresentam a teoria do retrenchment e a sua aplicação como uma extensão do método formal B. A seguir, introduz-se os conceitos relacionados a essa téc- nica aplicada a B e, posteriormente, a sua utilização para especificar a mudança de tipos e interface das operações durante o processo de desenvolvimento no método BSmart.

Retrenchment em B

Observa-se que o retrenchment é uma máquina B com a adição de alguns outros compo- nentes (figura 4.19), a saber, uma (1) cláusula RETRENCHES, contendo o nome da máquina ou refinamento objeto do retrenchement, uma (2) cláusula RETRIEVES que especifica a rela- ção entre os estados abstratos e concretos e (3) uma substituição generalizada composta pelas cláusulas LVAR, WITHIN e CONCEDES, que estende a substituição no corpo de uma operação, especificando as situações nas quais a operação concreta falha ao refinar a operação abstrata. Percebe-se que, diferentemente do refinamento em B, onde o invariante local e a relação en- tre os estados abstratos e concretos são ambos especificados no invariante do refinamento, no retrenchment, o invariante somente se aplica ao estado concreto.

Todos os elementos que descrevem um refinamento B estão disponíveis no retrenchment. Evidencia-se que podem ser utilizadas, do mesmo modo que uma máquina B comum, a cláusula de definição de conjuntos (SETS) e todas as cláusulas utilizadas na composição de máquinas.

Com relação às clausulas introduzidas pelo retrenchment, observa-se que a cláusula LVAR é opcional e deve ser utilizada apenas se for necessário declarar variáveis cujo escopo são as cláusulas WITHIN e CONCEDES. Uma vez declaradas, essas variáveis devem receber tipo e restrições aos seus valores em WITHIN.

MACHINE M_A(pmA) CONSTRAINTS PA(pmA) ... VARIABLES v_A INVARIANT Inv(vA) INITIALISATION Init(vA) OPERATIONS rA←− OPA(pA) = SA(vA, pA, rA) END MACHINE M_R(pmR) RETRENCHES MA(pmA) CONSTRAINTS PR(pmR) ... VARIABLES vR INVARIANT Inv(vR) RETRIEVES Ret(vA, vR) INITIALISATION Init(vR) OPERATIONS rR←− OPR(pR) = BEGIN SR(vR, pR, rR) LVAR R WITHIN W(pA, pR, vA, vR, R) CONCEDES C(vA, vR, rA, rR, R) END END

Figura 4.19: Máquina B padrão (esquerda) e máquina retrenchment (direita).

Evidencia-se que a cláusula WITHIN também pode ser utilizada, se necessário, para espe- cificar o fortalecimento da pré-condição de uma operação. Por sua vez, a cláusula CONCEDES presta-se ao papel de enfraquecer a pós condição de uma operação. Essas cláusulas adicionais podem ser precisamente descritas e compreendidas através da definição das obrigações de prova do retrenchment, o que será feito na próxima seção. Posteriormente, ilustrar-se-á a aplicação do retrenchmentao desenvolvimento BSmart de modo a permitir a verificação da mudança no tipo e na interface das operações da máquina inicial para a sua representação Java Card.

Obrigações de prova

As obrigações de prova do retrenchment podem ser classificadas como locais, ao se lidar apenas com informações do módulo de retrechment, ou conjuntas, no momento em que relaci- onam a máquina de retrenchment com o módulo B abstrato.

É interessante observar que as obrigações de prova locais em um módulo de retrenchment são as mesmas que aquelas encontradas em uma máquina B comum, a saber, o estabelecimento do invariante na inicialização e a preservação do estado especificado no invariante pelas opera-

ções, quando elas são aplicadas a estados nos quais a pré-condição da operação é satisfeita. A verificação dessas obrigações de prova garante a consistência interna do módulo.

Ao tratar-se das obrigações de provas conjuntas, a inicialização é similar ao que é encon- trado no refinamento tradicional (seção 3.2.1), exceto pelo fato de que se deve satisfazer o predicado na cláusula RETRIEVES, ao invés do INVARIANT. A obrigação de prova que deve ser verificada na inicialização do retrenchment é definida pela fórmula:

Obrigação de Prova 4.1

PA(pmA) ∧ PR(pmR) ⇒ [Init(vR)](¬[Init(vA)](¬Ret(vA, vR)))

As obrigações de prova para as operações são as que realmente definem o retrenchment. Como salientado no antecedente da fórmula da obrigação de prova 4.2, para cada operação, a validade do processo de verificação é condicionada às situações em que as propriedades especi- ficadas para os parâmetros do módulo (PA(pmA) e PR(pmR)), os invariantes abstratos (Inv(vA)) e

concretos (Inv(vR)) e a relação de “retrenchment” (Ret(vA, vR)) são satisfeitas. Essas condições

são similares ao que é feito para o refinamento tradicional. Por outro lado, de forma diferente do refinamento, no qual todo estado que pode ser atingido pelo modulo abstrato deve ser capaz de ser atingido pelo seu correspondente concreto, no retrenchment são as operações concretas que condicionam o processo de verificação.

Obrigação de Prova 4.2

PA(pmA) ∧ PR(pmR) ∧ (Inv(vA) ∧ Ret(vA, vR) ∧ Inv(vR))∧

trm(SR(vR, pR, rR)) ∧W (pA, pR, vA, vR, R)) ⇒ trm(SA(vA, pA, rA))∧

[SR(vR, pR, rR)](¬[SA(vA, pA, rA)](¬(Ret(vA, vR) ∨C(vA, vR, rA, rR, R))))

Destaca-se que a prevalência dos estados concretos sobre os abstratos é a característica do retrenchment que permite o comportamento mais permissivo quando comparado ao refina- mento tradicional. Enquanto agrega a vantagem ao retrechment de especificar uma operação no módulo concreto de forma mais flexível que no refinamento, essa característica o enfraquece, tornando-o uma abordagem de desenvolvimento menos rigorosa que o refinamento tradicional. Assim, no retrenchment, é possível existirem estados abstratos que não possam ser simulados no componente concreto. Isso aparece na obrigação de prova, com a terminação da operação con- creta (trm(SR(vR, pR, rR))) na hipótese e a terminação da operação abstrata (trm(SA(vA, pA, rA)))

Aspectos relacionados ao estado abstrato que não estão expressos na relação de retrench- ment(Ret(vA, vR)) podem ser especificados na cláusula WITHIN (W (pA, pR, vA, vR, A)), sendo

também o lugar de se relacionar as entradas de uma operação abstrata com a sua correspon- dente concreta, no caso, por exemplo, da mudança na interface entre elas. Por sua vez, no consequente da obrigação de prova tem-se o predicado da cláusula CONCEDES (C(v_A,v_R, r_A,r_R,R)). Ele permite especificar comportamentos adicionais relacionados aos estados concretos e abstratos e aos valores de saída da operação em situações nas quais a relação de retrenchment não seja satisfeita. Na obrigação de prova, esse comportamento é inse- rido através da disjunção do predicado concedes com o predicado da relação de retrenchment (Ret(v_A,v_R) ∨C(v_A,v_R,r_A,r_R,R)).

Retrenchment aplicado ao desenvolvimento Java Card

A figura 4.20 é uma representação de um retrenchment da especificação inicial (J_App) contendo apenas tipos compatíveis com Java Card do desenvolvimento BSmart. O componente que representa o estado do módulo é a variável jc_v, restrita ao sistema de tipos Java Card, o que é estabelecido no invariante, assim como feito para uma máquina B clássica. Na cláusula RETRIEVESdo retrenchment, é relacionado o estado abstrato (j_v) da máquina J_App com o estado concreto do retrenchment, armazenado na variável (jc_v). Para tanto, é utilizada a função de conversão java_of_jc, definida no componente InterfaceContext (seção 4.4.1), que associa o estado Java Card ao estado Java equivalente.

MACHINE JC_App_ret RETRENCHES J_App

SEES J_Context, JC_Context, InterfaceContext ABSTRACT_VARIABLES jc_v

INVARIANT jc_v ∈ JC_TYPE ∧ jc_inv ( jc_v ) = TRUE RETRIEVES j_v = java_of_jc ( jc_v )

INITIALISATION ANY val

WHERE val ∈ JC_TYPE ∧ jc_inv ( val ) = TRUE THEN jc_v := val

END OPERATIONS

jc_r← jc_operation ( jc_param ) = BEGIN

PRE jc_param ∈ JC_TYPE ∧ jc_pre ( jc_param ) = TRUE THEN jc_v := jc_stf ( jc_v , jc_param ) k

jc_r:= jc_ouf ( jc_v , jc_param ) END

WITHIN j_v := java_of_jc (jc_v ) END

No caso particular do retrenchment Java Card apresentado, a função de conversão de tipos Javapara Java Card é também inserida na cláusula WITHIN para possibilitar a verificação da equivalência entre os estados abstratos e concretos. A substituição (j_v := java_of_jc(jc_v)) evidencia que o retrenchment é válido, desde que ele e a máquina abstrata (J_App) sejam ca- pazes de efetuar transições de estado equivalentes, ainda que a interface e os tipos de dados recebidos pela operação do retrenchment tenham sido modificados.

Embora o retrenchment possa ser uma alternativa ao refinamento clássico, possibilitando desenvolvimentos que não seriam possíveis nesse modelo, ele possui como desvantagem o fato de permitir a verificação menos rigorosa que o refinamento. Além disso, a sua utilização ainda é inexpressiva e não há suporte de ferramentas maduro para ele. Nessa direção, uma iniciativa acadêmica é software Frog [FB07], desenvolvido como parte da tese de Frasier [Fra08]. Essa ferramenta propõe um framework para automatizar o suporte ao retrenchment. Inicialmente, o método formal Z [Spi92] é empregado como notação matemática para a especificação. Obriga- ções de prova são geradas no formato do provador de teoremas Isabelle [NPW10], que então efetua as verificações.

Ressalta-se que o retrenchment Java Card da figura 4.20 foi corretamente verificado utili- zando a ferramenta Atelier B. Nesse caso, o arquivo de obrigação de prova para o refinamento foi alterado de forma manual, de modo a acomodar o formato das obrigações de prova do re- trenchment.