A regra B-INV

Na figura 4.1 é apresentada a regra B-INV (basic invariance) que permite provar que uma fórmula de estado p é um invariante de um programa P.

  

Figure 4.1: Regra B-INV

A primeira premissa obriga que a condição inicial $\Phi$ implique p, i.é, p tem que ser válido nos estados iniciais do programa. Para entender a segunda regra são necessários alguns conceitos adicionais. Primeiro é preciso relembrar que $\mathcal{T}$ representa o conjunto de todas as transições de um programa. Temos também a seguinte equivalência:

$$\{p\} \mathcal{T} \{p\} \equiv \forall \tau \in \mathcal{T} \cdot \{p\} \tau \{p\}$$

Esta equivalência implica que a segunda premissa corresponda não a uma fórmula lógica, mas a um conjunto de fórmulas, uma por cada transição existente no FTS correspondente ao programa. Finalmente temos que

$$\{p\} \tau \{p\} \equiv \rho_\tau \land p \supset p'$$

onde $\rho_\tau$ corresponde à fórmula lógica que caracteriza a transição $\tau$ (ver tabela 3.1) e p' é a fórmula que se obtem substituindo em p todas as ocorrências de variáveis livres pelas respectivas versões linha. Dadas estas definições verifica-se que o objectivo da segunda premissa consiste em verificar que a validade de p é preservada por todas as transições.

Note-se que a validade da fórmula temporal $\Box p$ é verificada à custa da validade de um conjunto de fórmulas de estado não temporais.

Como exemplo da utilização desta regra considere que se pretendia provar, para o programa da figura 4.2, a validade da fórmula $\Box x \geq 0$. Neste caso, $p = x \geq 0$ e, sendo uma fórmula sem operadores temporais, podemos usar a regra B-INV para provar a sua validade.

  

Figure 4.2: Programa sequencial que soma 2 unidades

local x:int where x=0

l0: x := x+2;
l1:

A condição inicial $\Phi$ deste programa é

$$x=0 \land l0 \land \lnot l1$$

enquanto que a fórmula que caracteriza a sua única transição é definida por

$$l0 \land l1' \land \lnot l0' \land x'=x+2$$

Começando pela primeira premisa $\Phi \supset p$ temos

$$x=0 \land l0 \land \lnot l1 \supset x \geq 0$$

que é trivialmente válida. Como só temos uma transição a segunda premissa só dá origem à propriedade

$$l0 \land l1' \land \lnot l0' \land x'=x+2 \land x \geq 0 \supset x' \geq 0$$

que simplifica para $x \geq 0 \supset x+2 \geq 0$ que também é trivialmente válida. Pela regra B-INV concluimos que $\Box x \geq 0$ é P-válida para o programa da figura 4.2.