-
-
-
-
CENAPAD-MGCO
A seguir: Buffer: invariância de
Acima: Invariantes
Anterior: Invariantes
- Prova-se a invariância de um predicado P
de estado por indução:
- Base: provar que P é invariante
para computações de tamanho 1;
- Indução: supondo que P é
invariante para toda computação
de tamanho n, provar que P é invariante para toda computação
de tamanho n+1.
- Em outras palavras:
- Base: provar P(q0);
- Indução: para todo comando guardado
, mostrar
que
|  |
(1) |
(Obs.:
é a notação para o ``e'' lógico, e
para o ``ou''.)
- Ou: uma computação só pode ser prolongada por um comando
cuja guarda é válida, e só precisamos considerar prolongamentos
de computações P-invariantes.
Osvaldo Carvalho
-
Postscript -
Comentários?