- - - - CENAPAD-MGCO

A seguir: Buffer Limitado: Progresso Acima: Modelos Formais: Progresso Anterior: Equidade forte e fraca:

Produtor e Consumidor

Voltando ao buffer limitado: Prova de  

$$\left\vert produced \right\vert \geq l \ensuremath{ \; leads\!{\small -}\!to\;}\left\vert consumed \right\vert \geq l$$ (2)

para qualquer inteiro positivo l.

Para isto basta provar que  

$$\left\vert produced \right\vert \geq l \wedge \left\vert con... ... leads\!{\small -}\!to\;} \left\vert consumed \right\vert = k+1$$ (3)

Vemos aqui um exemplo de uma regra de fechamento interessante, com o uso de uma métrica :

• temos $l- \left\vert consumed \right\vert$ como uma métrica
• se a métrica for igual a 0, teremos atingido o progresso desejado;
• se a métrica for maior que 0, nós provamos que ela sempre diminui;
• uma métrica (obviamente) não possui uma sequência infinita decrescente e maior que zero

Portanto, para provar 6.2, é suficiente a prova de 6.3.