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

A seguir: Buffer Limitado: Progresso Acima: Aula 14: Programação Distribuída Anterior: Aula 14: Programação Distribuída

Modelos Formais - Continuação

Modelos Formais - Continuação

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 2, é suficiente a prova de 3.