- - - - CENAPAD-MGCO

A seguir: Modelos Formais: Conclusões Acima: Produtor e Consumidor Anterior: Produtor e Consumidor

Buffer Limitado: Progresso

Vamos precisar de ter como hipótese a execução de $\gamma_{1}$ e de $\gamma_{2}$ com equidade fraca.

Seja

$$P \equiv \left\vert produced \right\vert \geq l \wedge \left\vert consumed \right\vert = k < l$$

Temos

$$P = P \wedge (consumerState = hungry \vee consumerState = thinking)$$

Mas

$$consumerState = thinking \ensuremath{ \; leads\!{\small -}\!to\;}consumerState = hungry$$

via $\gamma_{1}$.Como $\left\vert produced \right\vert = \left\vert buffer \right\vert + \left\vert consumed \right\vert$P implica em $n = \left\vert buffer \right\vert \gt$, e portanto $P \ensuremath{ \; leads\!{\small -}\!to\;}\left\vert consumed \right\vert = k+1$ (via $\gamma_{2}$), como queríamos demonstrar.