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

A seguir: Buffer: é indutivo Acima: Variáveis Auxiliares Anterior: Buffer com variáveis auxiliares

Buffer: $P\equiv consumed \leq produced$ não é indutivo

Comando Prova
$\gamma_{1}$ e $\gamma_{3}$ evidente, pois consumed' = consumed e produced' = produced.
$\gamma_{4}$ Temos $consumed \leq produced$, consumed' =consumed e produced' = produced + product. Portanto, $consumed' \leq produced'$.
$\gamma_{2}$ Temos $consumed \leq produced$, produced' = produced mas consumed' = consumed + buffer.head().

Problema: P não é indutivo!


Osvaldo Carvalho