- - - - CENAPAD-MGCO

A seguir: Modelos Formais: Progresso Acima: Modelos Formais para Programas Anterior: Buffer: é indutivo

Atingibilidade: o mais forte invariante

• Dado um predicado P proposto como invariante de um sistema de transições, podemos

  1.

  Contestar a invariância , exibindo uma computação em que P é violado. Por exemplo, a invariância de $P\equiv n = 0$ é contestada por qualquer computação em que um item chegue a ser produzido.

  2.

  Provar a invariância , encontrando um predicado indutivo R mais forte que P.

• Esta segunda etapa não é fácil, devido aos seguintes resultados[Keller, 1976]:
  • Seja A o predicado que é válido para todos os estados atingíveis de um sistema de transições T;
  • Claramente A é indutivo, e é o mais forte invariante de T (qualquer predicado mais forte que A não é invariante)
  • Portanto, se P for um invariante, existe sempre um predicado indutivo R mais forte que P, que pode ser usado na prova
  • Mas como encontrar este invariante indutivo? Isto não é decidível, pois seria equivalente a resolver o problema da parada da máquina de Turing.
• Existem heurísticas para se encontrar um invariante indutivo, mas na prática, uma boa compreensão do algoritmo é essencial.