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

A seguir: Variáveis Auxiliares Acima: Invariantes Anterior: Buffer: invariância de

Invariantes indutivos e não indutivos

 

• Nós sabemos que $\left\vert buffer \right\vert \leq MAX$ é invariante; porque não foi possível provar isto?
• É que $\left\vert buffer \right\vert \leq MAX$ é invariante, mas não é indutivo , ou seja, é fraco como hipótese de indução. Ao prolongar uma computação, só deveríamos nos preocupar com computações cujo último estado é atingível.
• A equação 1 considera o invariante a ser provado como indicador de atingibilidade. Em casos como este, estamos considerando que estados com $\left\vert buffer \right\vert = MAX$e n < MAX são atingíveis, o que nós sabemos que não é verdade.
• Para provar a invariância de um predicado P não indutivo, prova-se a invariância de um predicado R tal que

  1.

  $R \Longrightarrow P$, e

  2.

  R é indutivo.

• No caso, um predicado indutivo satisfatório é

  $$R \equiv (\left\vert buffer \right\vert = n) \wedge ( 0 \leq n \leq MAX)$$

• É importante observar a relação que a prova guarda com a concepção do algoritmo: n é claramente um contador dos itens em buffer, fato esquecido na primeira tentativa, e resgatado no predicado indutivo.