3. BULGULAR YORUMLAR
3.1 Birinci Alt Probleme İlişkin Bulgular ve Yorumlar
A noção de substituição simples pode ser estendida para substituições mais elaboradas. O conjunto dessas novas substituições fornece ao especificador uma ferramenta poderosa para descrição do comportamento da especificação.
Na presente seção podem ser vistas importantes substituições generalizadas. O termo “subs- tituição generalizada” expressa a ideia de que a aplicabilidade de uma substituição pode ser ex- pandida ou restrita para se descrever e se verificar diversos novos comportamentos. É possível, por exemplo, impor restrições à aplicação de uma substituição e especificar a execução paralela de substituições.
Pré-condição A pré-condição especifica as propriedades que devem ser satisfeitas para a correta aplicação de uma operação. Seja P a pré-condição da operação, S a substituição em seu corpo, e I um predicado (normalmente o invariante da máquina), esta substituição pode ser formalmente descrita como:
[PRE P THEN S END]I ⇔ P ∧ [S]I
É importante observar que a validade de [S]I é condicionada ao predicado da pré-condição ser satisfeito. Caso a pré-condição não possa ser garantida, então não há garantia de que a máquina será levada para um estado válido após a aplicação da operação. Na fórmula abaixo, a obrigação de prova para uma operação é estendida, agora levando-se em conta que ela possui pré-condição.
I∧ P ⇒ [PRE P THEN S END]I
I∧ P ⇒ P ∧ [S]I, que pode ser reduzida para: I∧ P ⇒ [S]I
Informalmente, a fórmula acima afirma que, supondo a validade do invariante (a máquina encontra-se em um estado permitido) antes da aplicação da operação, e que ela seja aplicada
respeitando-se as restrições descritas na pré-condição, então o estado posterior à sua aplicação deve ser também válido, em respeito ao invariante da máquina.
Condicional A substituição condicional é formalmente descrita por:
[IF P THEN S ELSE T END]R ⇔ (P ⇒ [S]R) ∧ (¬P ⇒ [T ]R)
A aplicação da substituição S ou da substituição T é condicionada pela satisfação do predi- cado P. Nos casos em que P é verdadeiro, então S é a substituição efetuada, de outro modo, T será aplicada. A substituição condicional também possui uma forma curta, sem a parte ELSE. Nesse caso, apenas a substituição S é condicionada pelo predicado P.
Sem efeito (skip) A substituição “sem efeito”, ou simplesmente skip, apesar do seu nome, possui um papel importante. Ela é útil na definição de novas substituições, como no caso da substituição condicional que não possui a parte ELSE, além de ser um meio para se adiar a especificação do comportamento de uma operação. Assim, o comportamento é especificado somente posteriormente, em um refinamento da operação.
A substituição skip é formalizada pela regra: [skip]I ⇔ I
Como ilustração, a substituição condicional, quando utilizada sem a parte ELSE, pode ser definida do mesmo modo que a sua versão completa, apenas adicionando-se a substituição skip na parte ELSE.
IF P THEN S ELSE skip END ≡ IF P THEN S END
Paralela As substituições sob o escopo da substituição paralela são aplicadas “simultane- amente”. Ou seja, não é possível supor as noções de ordem e tempo na aplicação de cada substituição individualmente. Esta substituição normalmente é utilizada na especificação de mais de uma substituição em uma operação abstrata ou para se inicializar múltiplas variáveis utilizando-se uma combinação de substituições simples.
Não há regra específica para se obter a obrigação de prova para substituições sob o escopo da substituição paralela. Dessa forma, deve-se reescrever as substituições envolvidas até que o paralelismo seja removido [Sch01]. As regras básicas para a reescrita, sendo S e T substituições, xe y variáveis e E e F expressões, são:
skip:
Sk skip = S Comutatividade: Sk T = T k S
Substituição múltipla em paralelo:
(x1,..., xn:= E1,..., En) k (y1,..., ym:= F1,..., Fm)
= x1,..., xn, y1,..., ym:= E1,..., En, F1,..., Fm
A seguir descreve-se como exemplo as regras para as substituições de pré-condição e con- dicional quando em paralelo com outra substituição. As regras para as demais substituições generalizadas, por serem semelhantes, foram omitidas.
(PRE P THEN S END) k T = PRE P THEN S k T END
(IF E THEN S1ELSE S2END) k T = IF E THEN S1k T ELSE S2k T END
Escolha A substituição de escolha (bounded choice) permite descrever mais de um com- portamento válido para uma operação. O comportamento que será efetivamente implementado deve ser escolhido pelo especificador em um refinamento da operação. Formalmente, tem-se:
[CHOICE S OR T END]I ⇔ [S]I ∧ [T ]I
A conjunção de substituições na fórmula de escolha pode ser informalmente interpretada, afirmando-se: “Não importa qual substituição será escolhida pelo especificador, desde que ela respeite e preserve a correção do invariante”. Essa noção pode ser estendida para qualquer número de substituições em uma escolha.
Any Permite introduzir definições locais de variáveis em uma substituição. Seja v uma lista de nomes de variáveis e Q um predicado contendo o tipo e as condições que devem ser satisfeitas para a utilização das variáveis introduzidas. A substituição S estabelece o predicado P, sempre que for possível escolher uma valoração para as variáveis v, sob as restrições de Q, que tornem a substituição de S em P válida.
3.2 Refinamento
O refinamento é o módulo B utilizado para se redefinir a descrição do estado (dados) e do comportamento (operações) de uma máquina abstrata ou outro refinamento prévio. Ambos os refinamentos de dados e operações podem ser aplicados visando reduzir, de forma gradual no desenvolvimento, o não-determinismo de construções abstratas na direção de uma represen- tação concreta da especificação. No último nível de refinamento, a implementação, deve-se utilizar uma notação puramente determinística, fato esse que possibilita a tradução do desen- volvimento para uma linguagem de programação. Outra aplicação deste tipo de refinamento é o gerenciamento da complexidade das obrigações de prova em um módulo B. Usualmente, uma cadeia de refinamentos é desenvolvida, permitindo que pequenas mudanças sejam introduzidas a cada refinamento, reduzindo progressivamente a complexidade da especificação.
A figura 3.2 apresenta um esquema genérico de um módulo B de refinamento. O refina- mento é nomeado na cláusula REFINEMENT. O nome do módulo que está sendo refinado deve ser fornecido na cláusula REFINES. É possível introduzir novas variáveis na cláusula VARIA- BLESdo refinamento. As variáveis devem receber, no invariante, uma expressão de atribuição de tipo e restrições adicionais ao seu estado, assim como é feito para as variáveis abstratas. Entretanto, o invariante do refinamento possui um papel adicional. Nele deve-se relacionar o estado concreto do refinamento com o estado abstrato. Esse processo recebe o nome de rela- ção de refinamento, sendo concretizado através de invariantes de ligação (gluing invariants). Nessa relação, cada transição possível de ser feita no estado concreto deve corresponder a uma transição permitida para o modelo abstrato.
MACHINE MA VARIABLES vA INVARIANT InvA(vA) INITIALISATION InitA(vA) OPERATIONS rA←− OPA(pA) b= PRE PreA(vA, pA) THEN SA(vA, pA, rA) END END REFINEMENT MR REFINES MA VARIABLES vR INVARIANT InvR(vA, vR) INITIALISATION InitR(vR) OPERATIONS rR←− OPR(pR) b= PRE PreR(vR, pR) THEN SR(vR, pR, rR) END END
Salienta-se que as operações do refinamento estão sujeitas a regras restritivas que devem ser obedecidas para possibilitar o refinamento, quais sejam, (i) o refinamento deve preservar o mesmo número de operações do módulo refinado e (ii) a assinatura da operação abstrata não pode ser modificada no refinamento. A restrição (ii) significa que o nome da operação e a ordem, nome e tipo de seus parâmetros de entrada e valores de retorno não podem ser modificados. Essas restrições podem trazer certas dificuldades ao desenvolvimento de software. No capítulo 4, discute-se duas soluções para contornar a restrição de mudança de interface no refinamento, o que beneficia diretamente o refinamento no método BSmart.