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

A seguir: Buffer com variáveis auxiliares Acima: Aula 11 - Modelos Anterior: Invariantes indutivos e não

Variáveis Auxiliares

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.