Regras da Verificação de Programas

As regras da verificação de programas estão organizadas (essencialmente) pelos tipos de instruções.

Ciclos e Programas Parciais

Num triplo de Hoare, $[[a]]\text{P}[[b]]$, a verificação da pós-condição pressupõe que $\text{P}$ termina quando $\models a$.

Entre os tipos de instruções, apenas os ciclos podem contribuir para programas que não terminam; Um programa apenas com instruções "cópia" ou "condição" sem ciclos termina sempre.

Como o problema da paragem é indecidível, isto é, não há um algoritmo para classificar um programa como total ou parcial, as regras de verificação que envolvem ciclos (onde está o "problema" da paragem) devem contemplar ambos os casos.

De facto, existe uma regra para ciclos totais e outra regra para ciclos parciais.

O tratamento dos ciclos totais está fora do âmbito desta disciplina e vai-se usar apenas a regra do caso parcial nos ciclos.

A razão desta escolha está na complexidade adicional de tratar o caso total. Os ciclos, como estão apresentados, permitem programas parciais e, claro, também programas totais.

Uma forma de garantir que um ciclo termina consiste em usar ciclos limitados. Por exemplo, a sintaxe do C permite

for (int i = 0; i < 10; i++) {
    // instruções que não afetam i
}

Claro, isto é um caso particular de ciclos ilimitados:

#![allow(unused)]
fn main() {
i = 0;
while i < 10 {
    // instruções que não afetam i
    i = i + 1;
}
}

Regras para a Verificação de Programas Parciais

$$⊢\text{impl}\text{seq}\text{copy}\text{cond}\text{loop}$$

Implicação

Definição ($\text{impl}$)

$$\frac{\begin{array}{c}{⊢}_{\text{AR}}a\to u[[u]]\text{P}[[v]]{⊢}_{\text{AR}}v\to b\end{array}}{[[a]]\text{P}[[b]]}\left(\text{impl}\right)$$

Nesta regra:

• $a,u,v,b$ são fórmulas FOL+Aritmética.
• $H{⊢}_{\text{AR}}t$ significa que existe uma prova de $t$ com hipóteses $H$ na lógica FOL+Aritmética.
• P é um programa.

Esta é uma regra de "conveniência", que permite generalizar a pré-condição e restringir a pós-condição.

Sequência

Sequência ($\text{seq}$)

$$\frac{\begin{array}{c}[[a]]\text{P}[[c]][[c]]\text{Q}[[b]]\end{array}}{[[a]]\text{P ; Q}[[b]]}\left(\text{seq}\right)$$

Nesta regra:

• $a,b,c$ são fórmulas FOL+Aritmética.
• P e Q são programas.

Intuitivamente:

1. Se $\models a$ antes de $\text{P}$ e $\models c$ depois,
2. e se $\models c$ antes de $\text{Q}$ e $\models b$ depois;
3. Estão, quando $\models a$ antes de $P\text{;}Q$ também $\models b$ depois: $$[[a]]P[[c]]Q[[b]]$$

Cópia

Cópia ($\text{copy}$)

$$\frac{\begin{array}{}\end{array}}{[[a\left\{x/E\right\}]]\text{x = E}[[a]]}\left(\text{copy}\right).$$

Nesta regra:

• $a$ é uma fórmula FOL+Aritmética.
• $E$ é um termo aritmético.
• $a\left\{x/E\right\}$ resulta de substituir, em $a$, algumas ocorrências da variável $x$ por $E$.

Exemplo. Provas em Tabela

Mostrar que

$$⊢[[y=5]]\text{x = y + 1}[[x=6]].$$

Temos de usar a regra

$$\frac{\begin{array}{}\end{array}}{[[a\left\{x/E\right\}]]\text{x = E}[[a]]}\left(\text{copy}\right)$$

Para esta regra ser corretamente aplicada é necessário identificar o termo $E$ e a fórmula $a$.

Uma prova em tabela é:

1. Na primeira linha está a pré-condição do triplo (prec) e na última linha está a pós-condição do triplo.
2. A segunda linha $y+1=6$ resulta da primeira por aplicação das regras da aritmética (aritm).
3. Na terceira linha está (apenas) a instrução do triplo.
4. Finalmente, a última linha resulta de aplicar a regra $\text{copy}$.

Mas ficam algumas dúvidas:

• Qual a justificação para a linha 2? É necessária?
• Donde vêm a fórmula $a$ e o termo $E$? O que se passa com a substituição $a\left\{x/E\right\}$?

Como identificar a fórmula $a$ e o termo $E$ usados na regra $\text{copy}$.

1. De acordo com a regra, $a$ deve ser a pós-condição de uma instrução da forma x = E.
2. O que pretendemos com esta regra é obter a fórmula $x=6$. Portanto, $a$ deve ser $x=6$.
3. Falta o $E$. A instrução "real" é x = y + 1. Portanto, $E$ deve ser $y+1$.
4. Isso significa que na prova deve estar a fórmula $y+1=6$, que resulta de $a\left\{x/y+1\right\}$.
5. Por isso é usado o teorema ${⊢}_{AR}y=5\to y+1=6$ da aritmética e a regra $\text{impl}$.
   • Em casos diretos, como este, pode usar-se a "pseudo-regra" $\text{aritm}$ para simplificar a prova.

Mais rigorosamente, o que aquela tabela apresenta é a seguinte prova formal:

$$\frac{\begin{array}{c}{⊢}_{AR}y=5\to y+1=6\frac{\begin{array}{}\end{array}}{[[(x=6)\left\{x/y+1\right\}]]\text{x = y + 1}[[x=6]]}\left(\text{copy}\right){⊢}_{AR}x=6\to x=6\end{array}}{[[y=5]]\text{x = y + 1}[[x=6]]}\left(\text{impl}\right)$$

Este exemplo ilustra a seguinte eurística para as provas de verificação:

As linhas de uma prova lêem-se "de cima para baixo" mas escrevem-se "de fora para dentro"

O que isto significa é que as seguintes regras ajudam a fazer uma prova:

1. Começar por escrever as hipóteses ou pré-condições dadas e a conclusão ou pós-condição pretendida.
2. "Descer" a partir das linhas superiores enquanto as conclusões são diretas.
3. "Subir" das linhas inferiores enquanto a hipóteses necessárias são diretas.

Exemplos da regra $\text{copy}$.

1. $[[2=2]]\text{x = 2}[[x=2]]$
2. $[[2=4]]\text{x = 2}[[x=4]]$
3. $[[2=y]]\text{x = 2}[[x=y]]$
4. $[[2>0]]\text{x = 2}[[x>0]]$
5. $[[x+1=2]]\text{x = x + 1}[[x=2]]$
6. $[[x+1=y]]\text{x = x + 1}[[x=y]]$
7. $[[x+1+5=y]]\text{x = x + 1}[[x+5=y]]$
8. $[[x+1<0\wedge y>0]]\text{x = x + 1}[[x>0\wedge y>0]]$
9. $[[y=y]]\text{x = y}[[x=y]]$

Condicional

Condicional ($\text{cond}$)

$$\frac{\begin{array}{c}[[a\wedge C]]\text{P}[[b]][[a\wedge \neg C]]\text{Q}[[b]]\end{array}}{[[a]]\text{if C { P } else { Q }}[[b]]}\left(\text{cond}\right).$$

Nesta regra:

• $a,b$ e $C$ são fórmulas FOL + Aritmética.
• P e Q são programas, respetivamente os ramos positivo e negativo da instrução condicional.

Exemplo. $⊢[[\top ]]\text{Max}[[z=max(x,y)]]$

Seja Max o programa

#![allow(unused)]
fn main() {
if x > y {
    z = x
} else {
    z = y
}
}

Recapitulando a definição de $max$ da aritmética:

$$\begin{array}{rl}z=max(x,y)\leftrightarrow & \left(z=x\vee z=y\right)\\ & \wedge z\ge x\\ & \wedge z\ge y\end{array}$$

Ciclo Parcial e Invariante

Definição ($\text{loop}$, Invariante) $$\frac{\begin{array}{c}[[a\wedge C]]\text{P}[[a]]\end{array}}{[[a]]\text{while C {P}}[[a\wedge \neg C]]}\left(\text{loop}\right).$$

Uma invariante do ciclo $\text{while}C\text{{}P\text{}}$ é qualquer fórmula $a$ tal que $$\models [[a\wedge C]]\text{P}[[a]].$$

Isto é,

A fórmula $a$ é um invariante do ciclo $\text{while}C\text{{}P\text{}}$ se para qualquer estado $e$ tal que $e⊢a,C$, quando $P$ é executado no estado $e$ e termina, no estado final, $f$, ainda $f\models a$.

Por outras palavras, um invariante de um ciclo é uma condição que é válida antes e depois da computação do corpo do ciclo. Pode acontecer que durante essa computação a condição deixe de ser válida desde que, no fim, volte a sê-lo.

Exemplo. Verificação de um programa para calcular $x!$.

Mostre que $\models [[x\ge 0]]\text{Fac1}[[y=x!]]$ em que Fac1 é o programa

#![allow(unused)]
fn main() {
y = 1;
z = 0;
while z != x {
    z = z + 1;
    y = y * z;
}
}

Para este exemplo é preciso recapitular a seguinte propriedade da aritmética:

$$\{\begin{array}{ll}0!& =1\\ (x+1)!& =(x+1)x!\end{array}$$