- - - - CENAPAD-MGCO

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

Buffer: $R \equiv consumed + buffer = produced$ é indutivo

• Claramente $R \Longrightarrow P$, e R é válido inicialmente;

Comando Prova

$$\gamma_{1} \gamma_{3}$$ Não afetam as variáveis em R

$$\gamma_{2}$$ n > 0, e portando buffer = a+x, onde a é um char, e x uma sequência (talvez nula) de char. Sendo assim, temos consumed' = consumed + a, buffer' = x e portanto consumed' + buffer' = consumed + a + x = consumed + buffer = produced = produced'.

$$\gamma_{4}$$ consumed'=consumed, buffer' = buffer + product, e produced' = produced + product. Portanto consumed' + buffer' = produced'.