UFMG - Pós-graduação em Ciência da Computação - Programação Paralela

A seguir: Buffer: invariância de Acima: Invariantes Anterior: Invariantes

Prova de Invariância

• 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(q₀);
  • Indução: para todo comando guardado $\gamma = (g,a)$, mostrar que  

    $$\forall q, q' \in Q, q' = a(q), P(q) \wedge g(q) \Longrightarrow P(q')$$ (1)

    (Obs.: $\wedge$ é a notação para o ``e'' lógico, e $\vee$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.