Variáveis Auxiliares

Vamos agora tentar provar que a sequência de itens consumidos é sempre um prefixo da sequência de itens produzidos.
Não temos como expressar esta propriedade como um predicado de estado (uma função $P:Q \rightarrow \{true, false\}$ );
Existem duas soluções para este problema:
- enriquecer a linguagem de expressão de propriedades do conjunto de computações de um sistema de transições, ou
- aumentar o sistema com variáveis auxiliares [Owick and Gries, 1976], como faremos aqui;
variáveis auxiliares são variáveis de estado que registram alguma história da execução, mas não afetam o sistema, e portanto não são (necessariamente) implementadas;
Um subconjunto V de variáveis de estado é auxiliar se

1.
variáveis em V nunca aparecem em qualquer guarda de comando, e
2.
o valor de uma variável em V nunca afeta o valor de uma variável fora de V
Em outras palavras, as variáveis em V:
- só aparecem em comandos de atribuição, e
- quando aparecem no lado direito do comando de atribuição, a variável alvo também é auxiliar.

Next: Buffer com variáveis auxiliares Up: Modelos Formais para Programas Previous: Invariantes indutivos e não