Buffer com variáveis auxiliares

CENAPAD-MGCO

A seguir: Buffer: não é indutivo Acima: Variáveis Auxiliares Anterior: Variáveis Auxiliares

Buffer com variáveis auxiliares

Variáveis acrescentadas:

Variável	Valores	Valor Inicial
consumed	char^*	$\ensuremath{\epsilon}$
produced	char^*	$\ensuremath{\epsilon}$

Comandos:

Com Guarda Ação

$\gamma_{1}$ consumerState = thinking consumerState = hungry;

$\gamma_{2}$ consumerState = hungry $\wedge$ n > 0 consumption = buffer.head(); buffer = buffer.tail(); n = n - 1; consumerState = thinking; consumed.append(consumption);

$\gamma_{3}$ producerState = thinking producerState = hungry; product = randomChar();

$\gamma_{4}$ producerState = hungry $\wedge$ n < MAX buffer.append(product); n = n + 1; producerState = thinking; consumed.append(product);

Osvaldo Carvalho

Postscript

Comentários?

Com	Guarda	Ação
$\gamma_{1}$	consumerState = thinking	consumerState = hungry;
$\gamma_{2}$	consumerState = hungry $\wedge$ n > 0	consumption = buffer.head(); buffer = buffer.tail(); n = n - 1; consumerState = thinking; consumed.append(consumption);
$\gamma_{3}$	producerState = thinking	producerState = hungry; product = randomChar();
$\gamma_{4}$	producerState = hungry $\wedge$ n < MAX	buffer.append(product); n = n + 1; producerState = thinking; consumed.append(product);