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, $\ho{a}{P}{b}$, a verificação da pós-condição pressupõe que $\kw{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
$$ \Huge \begin{matrix} \vdash & \ndrname{impl} & \ndrname{seq}\cr \ndrname{copy} & \ndrname{cond} & \ndrname{loop} \end{matrix} $$
Implicação
Definição ($\ndrname{impl}$)
$$ \ndrule { \vdash_\text{AR} a \to u \quad \ho{u}{P}{v} \quad \vdash_\text{AR} v \to b } { \ho{a}{P}{b} } { \ndrname{impl} } $$
Nesta regra:
- $a, u, v, b$ são fórmulas FOL+Aritmética.
- $H \vdash_{\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 restringir a pré-condição e generalizar a pós-condição.
Sequência
Sequência ($\ndrname{seq}$)
$$ \ndrule{ \ho{a}{P}{c} \quad \ho{c}{Q}{b} } { \ho{a}{P ; Q}{b} } { \ndrname{seq} } $$
Nesta regra:
- $a, b, c$ são fórmulas FOL+Aritmética.
PeQsão programas.
Intuitivamente:
- Se $\models a$ antes de $\kw{P}$ e $\models c$ depois,
- e se $\models c$ antes de $\kw{Q}$ e $\models b$ depois;
- Estão, quando $\models a$ antes de $\pseq{P}{Q}$ também $\models b$ depois: $$ \cond{a} P \cond{c} Q \cond{b} $$
Cópia
Cópia ($\ndrname{copy}$)
$$ \ndrule{} { \ho{a\subst{x}{E}}{x = E}{a} } {\ndrname{copy}}. $$
Nesta regra:
- $a$ é uma fórmula FOL+Aritmética.
- $E$ é um termo aritmético.
- $a\subst{x}{E}$ resulta de substituir, em $a$, algumas ocorrências da variável $x$ por $E$.
Exemplo. Provas em Tabela
Mostrar que
$$ \vdash \ho{y = 5}{x = y + 1}{x = 6}. $$
Temos de usar a regra
$$ \ndrule{} {\ho{a\subst{x}{E}}{x = E}{a}} {\ndrname{copy}} $$
Para esta regra ser corretamente aplicada é necessário identificar o termo $E$ e a fórmula $a$.
Uma prova em tabela é:
| L | Instrução | Fórmula | Regra | Hs | Obs. |
|---|---|---|---|---|---|
| 1 | $y = 5$ | prec | pré-condição | ||
| 2 | $y + 1 = 6$ | aritm | 1 | aritmética | |
| na linha anterior | |||||
| 3 | x = y + 1 | ||||
| 4 | $x = 6$ | copy | 2, 3 | $a$ é a fórmula | |
| “$x = 6$” |
- Na primeira linha está a pré-condição do triplo (prec) e na última linha está a pós-condição do triplo.
- A segunda linha $y + 1 = 6$ resulta da primeira por aplicação das regras da aritmética (aritm).
- Na terceira linha está (apenas) a instrução do triplo.
- Finalmente, a última linha resulta de aplicar a regra $\ndrname{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\subst{x}{E}$?
Como identificar a fórmula $a$ e o termo $E$ usados na regra $\ndrname{copy}$.
- De acordo com a regra, $a$ deve ser a pós-condição de uma instrução da forma
x = E. - O que pretendemos com esta regra é obter a fórmula $x = 6$. Portanto, $a$ deve ser $x = 6$.
- Falta o $E$. A instrução “real” é
x = y + 1. Portanto, $E$ deve ser $y + 1$. - Isso significa que na prova deve estar a fórmula $y + 1 = 6$, que resulta de $a\subst{x}{y + 1}$.
- Por isso é usado o teorema $\vdash_{AR} y = 5 \to y + 1 = 6$ da aritmética e a regra $\ndrname{impl}$.
- Em casos diretos, como este, pode usar-se a “pseudo-regra” $\ndrname{aritm}$ para simplificar a prova.
Mais rigorosamente, o que aquela tabela apresenta é a seguinte prova formal:
$$ \scriptsize \ndrule{ \vdash_{AR} y = 5 \to y + 1 = 6 \quad \ndrule{} {\ho{(x = 6)\subst{x}{y + 1}}{x = y + 1}{x = 6}} {\ndrname{copy}} \quad \vdash_{AR} x = 6 \to x = 6 }{ \ho{y = 5}{x = y + 1}{x = 6}}{\ndrname{impl}} $$
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:
- Começar por escrever as hipóteses ou pré-condições dadas e a conclusão ou pós-condição pretendida.
- “Descer” a partir das linhas superiores enquanto as conclusões são diretas.
- “Subir” das linhas inferiores enquanto a hipóteses necessárias são diretas.
Exemplos da regra $\ndrname{copy}$.
- $\ho{\alert{2} = 2}{x = 2}{\alert{x} = 2}$
- $\ho{\alert{2} = 4}{x = 2}{\alert{x} = 4}$
- $\ho{\alert{2} = y}{x = 2}{\alert{x} = y}$
- $\ho{\alert{2} > 0}{x = 2}{\alert{x} > 0}$
- $\ho{\alert{x + 1} = 2}{x = x + 1}{\alert{x} = 2}$
- $\ho{\alert{x + 1} = y}{x = x + 1}{\alert{x} = y}$
- $\ho{\alert{x + 1} + 5 = y}{x = x + 1}{\alert{x} + 5 = y}$
- $\ho{\alert{x + 1} < 0 \land y > 0}{x = x + 1}{\alert{x} > 0 \land y > 0}$
- $\ho{\alert{y} = y}{x = y}{\alert{x} = y}$
Condicional
Condicional ($\ndrname{cond}$)
$$ \ndrule{ \ho{a \land C}{P}{b} \hspace{4em} \ho{a \land \neg C}{Q}{b} } { \ho{a}{if C { P } else { Q }}{b} } {\ndrname{cond}}. $$
Nesta regra:
- $a, b$ e $C$ são fórmulas FOL + Aritmética.
PeQsão programas, respetivamente os ramos positivo e negativo da instrução condicional.
Exemplo. $\vdash \ho{\top}{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{aligned} z = \max(x,y) \quad \liff & \quad \del{z = x \lor z = y} & \land \cr & \quad z \geq x & \land \cr & \quad z \geq y \end{aligned} $$
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $\top$ | prec | ||
| 2 | if x > y { | ||||
| ? | |||||
| ? | $\hspace{2em}$z = x | ||||
| ? | |||||
| ? | } else { | ||||
| ? | |||||
| ? | $\hspace{2em}$z = y | ||||
| ? | |||||
| ? | } | ||||
| ? | $\begin{matrix}{\del{z = x \lor z = y} \land \cr z \geq x \land z \geq y}\end{matrix}$ | cond | 2, ? - ?, ? - ? |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $\top$ | prec | ||
| 2 | if x > y { | ||||
| ? | |||||
| ? | $\hspace{2em}$z = x | ||||
| ? | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | têm de ser iguais | ||
| ? | } else { | ||||
| ? | |||||
| ? | $\hspace{2em}$z = y | ||||
| ? | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | têm de ser iguais | ||
| ? | } | ||||
| ? | $\begin{matrix}{\del{z = x \lor z = y} \land \cr z \geq x \land z \geq y}\end{matrix}$ | cond | 2, ? - ?, ? - ? | têm de ser iguais |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $\top$ | prec | ||
| 2 | if x > y { | ||||
| 3 | $x > y$ | posb | guarda | ||
| ? | $\hspace{2em}$z = x | ||||
| ? | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | |||
| ? | } else { | ||||
| 8 | $y \geq x$ | negb | negação da guarda | ||
| ? | $\hspace{2em}$z = y | ||||
| ? | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | |||
| ? | } | ||||
| ? | $\begin{matrix}{\del{z = x \lor z = y} \land \cr z \geq x \land z \geq y}\end{matrix}$ | cond | 2, ? - ?, ? - ? |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $\top$ | prec | ||
| 2 | if x > y { | ||||
| 3 | $x > y$ | posb | |||
| 4 | $\alert{\del{x = x \lor x = y} \land x \geq x \land x \geq y}$ | ? | $\alert{a\subst{z}{x}}$ | ||
| 5 | $\hspace{2em}$z = x | ||||
| 6 | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | $a$ | ||
| 7 | } else { | ||||
| 8 | $y \geq x$ | negb | negação da guarda | ||
| ? | $\hspace{2em}$z = y | ||||
| ? | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | |||
| ? | } | ||||
| ? | $\begin{matrix}{\del{z = x \lor z = y} \land \cr z \geq x \land z \geq y}\end{matrix}$ | cond | 2, ? - ?, ? - ? |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $\top$ | prec | ||
| 2 | if x > y { | ||||
| 3 | $x > y$ | posb | |||
| 4 | ${\del{x = x \lor x = y} \land x \geq x \land x \geq y}$ | impl | |||
| 5 | $\hspace{2em}$z = x | ||||
| 6 | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | |||
| 7 | } else { | ||||
| 8 | $y \geq x$ | negb | |||
| 9 | $\alert{\del{y = x \lor y = y} \land y \geq x \land y \geq y}$ | impl | $\alert{a\subst{z}{y}}$ | ||
| 10 | $\hspace{2em}$z = y | ||||
| 11 | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | copy | $a$ | ||
| 12 | } | ||||
| 13 | $\begin{matrix}{\del{z = x \lor z = y} \land \cr z \geq x \land z \geq y}\end{matrix}$ | cond | 2, ? - ?, ? - ? |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $\top$ | prec | ||
| 2 | if x > y { | ||||
| 3 | $x > y \land x = x$ | posb | |||
| 4 | $\hspace{2em}$z = x | ||||
| 5 | $x > y \land z = x$ | copy | |||
| 6 | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | impl | |||
| 7 | } else { | ||||
| 8 | $y \geq x \land y = y$ | negb | |||
| 9 | $\hspace{2em}$z = y | ||||
| 10 | $y \geq z \land z = y$ | copy | |||
| 11 | ${\del{z = x \lor z = y} \land z \geq x \land z \geq y}$ | impl | |||
| 12 | } | ||||
| 13 | $\begin{matrix}{\del{z = x \lor z = y} \land \cr z \geq x \land z \geq y}\end{matrix}$ | cond | 2, 3 - 6, 8 - 11 |
Ciclo Parcial e Invariante
Definição ($\ndrname{loop}$, Invariante)
$$ \ndrule{ \ho{a \land C}{P}{a} } { \ho{a}{\ploop{C}{P}}{a \land \neg C} } {\ndrname{loop}}. $$
Uma invariante do ciclo $\ploop{C}{P}$ é qualquer fórmula $a$ tal que $$\models \ho{a \land C}{P}{a}.$$
Isto é,
A fórmula $a$ é um invariante do ciclo $\ploop{C}{P}$ se para qualquer estado $e$ tal que $e \vdash 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 \ho{x \geq 0}{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{cases} 0! &= 1 \cr (x + 1)! &= (x + 1)x! \end{cases} $$
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $x \geq 0$ | prec | ||
| 2 | y = 1; | ||||
| ? | copy | ||||
| ? | z = 0; | ||||
| ? | copy | ||||
| ? | $\alert{a}$ | ||||
| ? | while z != x { | ||||
| ? | step | $z \not=x \land \alert{a}$ | |||
| ? | $\hspace{2em}$z = z + 1; | ||||
| ? | copy | ||||
| ? | $\hspace{2em}$y = y * z; | ||||
| ? | copy | ||||
| ? | $\alert{a}$ | ||||
| ? | } | ||||
| ? | loop | ?, ? - ? | $z = x \land \alert{a}$ | ||
| ? | $y = x!$ |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $x \geq 0$ | prec | ||
| 2 | $ 1 = 1 $ | impl | $\models_{AR} 1 = 1$ | ||
| 3 | y = 1; | ||||
| 4 | $ y = 1 $ | copy | |||
| 5 | $ 0 = 0 $ | impl | $\models_{AR} 0 = 0$ | ||
| 6 | z = 0; | ||||
| 7 | $ z = 0 $ | copy | |||
| 8 | $\alert{a} \land z \leq x$ | impl | $1 = 0! \to \underbrace{y = z!}_{\alert{a}?}$ | ||
| 9 | while z != x { | ||||
| 11 | $\alert{a} \land z \not= x$ | step | $z \leq x$ | ||
| ? | $\hspace{2em}$z = z + 1; | ||||
| ? | copy | ||||
| ? | $\hspace{2em}$y = y * z; | ||||
| ? | copy | ||||
| ? | $\alert{a}$ | ? | |||
| ? | } | ||||
| ? | $\alert{a} \land z = x$ | loop | ?, ? - ? | ||
| ? | $y = x!$ | impl |
| L. | Instrução | Fórmula | Regra | Hipóteses | Observação |
|---|---|---|---|---|---|
| 1 | $\phantom{\hspace{6em}}$ | $x \geq 0$ | prec | ||
| 2 | $ 1 = 1 $ | impl | $\models_{AR} 1 = 1$ | ||
| 3 | y = 1; | ||||
| 4 | $ y = 1 $ | copy | |||
| 5 | $ 0 = 0 $ | impl | $\models_{AR} 0 = 0$ | ||
| 6 | z = 0; | ||||
| 7 | $ z = 0 $ | copy | |||
| 8 | $\alert{y = z!} \land z \leq x$ | impl | $1 = 0! \to y = z!$ | ||
| 9 | while z != x { | ||||
| 11 | $\alert{y = z!} \land z \not= x$ | step | $z \leq x$ | ||
| 12 | $y(z + 1) = (z + 1)z!$ | impl | |||
| 13 | $\hspace{2em}$z = z + 1; | ||||
| 14 | $yz = z(z-1)!$ | copy | $z = (z + 1 ) - 1$ | ||
| 15 | $\hspace{2em}$y = y * z; | ||||
| 16 | $y = z(z-1)!$ | copy | |||
| 17 | $\alert{y = z!}$ | impl | |||
| 18 | } | ||||
| 19 | $\alert{y = z!} \land z = x$ | loop | 9, 11-17 | ||
| 20 | $y = x!$ | impl |