A regra G-INV

Existem situações em que a regra B-INV não se pode aplicar directamente. Por exemplo, considere que se pretendia provar, também para o programa da figura 4.2, a validade da seguinte fórmula:

$$l1 \Rightarrow x=2$$

Como já foi visto, esta fórmula é equivalente a

$$\Box (l1 \supset x=2)$$

e como tal pode ser usada a regra B-INV para provar a sua validade. Aplicando essa regra temos as seguintes propriedades para provar:

$$x=0 \land l0 \land \lnot l1 \supset (l1 \supset x=2)$$

$$l0 \land l1' \land \lnot l0' \land x'=x+2 \land (l1 \supset x=2) \supset (l1' \supset x'=2)$$

A primeira é válida pois, sendo $\lnot l1$ verdadeiro, a implicação $l1 \supset x=2$ é trivialmente verdadeira. Na segunda, como l1' é válida, a fórmula pode ser simplificada para $l0 \land l1' \land \lnot l0' \land (l1 \supset x=2) \supset x+2=2$, cuja validade implica a provar a validade de $l0 \supset x=0$. Embora seja óbvio que esta fórmula é uma fórmula de estado válida para o programa em questão, ela não é uma fórmula de estado válida para qualquer programa e esse facto impede a conclusão da prova usando simplesmente a regra B-INV. Numa fórmula temporal $\Box p$ em que isto não aconteça. i.é, aquelas que podem ser provadas por aplicação directa da regra B-INV, devido ao facto de as premisas resultantes serem fórmulas de estado válidas em qualquer programa, a fórmula p é designada como indutiva.

Para contornar estas situações podem ser usadas duas estratégias:

1.

Tentar provar uma propriedade mais "forte", ou

2.

Usar uma prova incremental, utilizando invariantes previamente verificados.

A primeira estratégia baseia-se na regra da monotonia da invariância (denominada MON-I) que é definida como:

$\Box p$

$p \supset q$

$\Box q$

Esta regra indica que, para provar a invariância de uma propriedade q é suficiente provar a invariância de uma propriedade p que a implique. Tendo em atenção esta regra, a primeira estratégia pode ser apresentada da seguinte forma: caso se pretenda provar a invariância de uma propriedade p que não seja indutiva é suficiente provar a invariância de uma propriedade mais "forte" (i.é, que a implique) que seja inductiva. Esta estratégia consiste na combinação da regra B-INV com a regra MON-I e é sintetizada numa nova regra designada G-INV (de general invariance) apresentada na figura .

  

Figure 4.3: Regra G-INV

De notar que esta estratégia pode, em princípio, ser sempre adoptada, pois existe um teorema que afirma que, se p é um invariante de um programa, então existe sempre uma fórmula inductiva $\varphi$ mais "forte" que p.

Para utilizarmos esta estratégia para provar a propriedade $\Box (l1 \supset x=2)$ é necessário encontar uma propriedade indutiva mais forte que a implique. Uma estratégia que resulta em muitas situações consiste em fazer uma conjunção da propriedade a provar com a fórmula que impedia a sua prova com a regra B-INV, neste caso $l0 \supset x=0$. Assim, iremos assumir $\varphi$ como:

$$(l1 \supset x=2) \land (l0 \supset x=0)$$

Aplicando a regra G-INV temos que a primeira premissa é definida pela fórmula

$$(l1 \supset x=2) \land (l0 \supset x=0) \supset (l1 \supset x=2)$$

que é trivialmente válida. A segunda premissa é

$$x=0 \land l0 \land \lnot l1 \supset (l1 \supset x=2) \land (l0 \supset x=0)$$

que por razões semelhantes às já apresentadas é também válida. Finalmente temos

$$l0 \land l1' \land \lnot l0' \land x'=x+2 \land (l1 \supset x... ...upset x=0) \supset (l1' \supset x'=2) \land (l0' \supset x'=0)$$

que pode ser simplificada para

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

que já é uma fórmula de estado genericamente válida. Desta forma se conclui a validade de $\Box (l1 \supset x=2)$ através da regra G-INV.

A segunda estratégia para provar a invariância de uma propriedade não inductiva p consiste em encontrar um invariante auxiliar q e utilizar depois a propriedade q como hipótese na prova de p usando a regra B-INV. Esta estratégia é exemplificada pela seguinte regra:

$\Box q$

$\Phi \supset p$

$\{q \land p\} \mathcal{T} \{p\}$

$\Box p$

No caso do exemplo anterior, para aplicar esta estratégia é necessário definir primeiro qual o invariante auxiliar a usar. Assumindo que $q = l0 \supset x=0$ é esse invariante (fica como exercício fazer a sua prova), resta provar que

$$x=0 \land l0 \land \lnot l1 \supset (l1 \supset x=2)$$

e

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

são fórmulas válidas. Como já vimos a primeira é válida e a segunda simplifica para

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

que também é uma fórmula válida.

A principal vantagem da segunda estratégia é a sua modularidade, i.é, em cada momento temos objectivos de prova mais simples e é possível reutilizar os invariantes já verificados noutras provas. No entanto nem sempre é possível proceder a uma prova incremental devido à dificuldade de encontrar invariantes auxiliares inductivos. Nestes casos a única hipótese é utilizar a primeira estratégia. De referir que uma prova incremental pode sempre ser substituída por uma prova com a regra G-INV, embora o contrário não seja sempre verdade.