- - - - CENAPAD-MGCO

A seguir: Invariantes indutivos e não Acima: Invariantes Anterior: Buffer: invariância de

Buffer: invariância de $P \equiv \left\vert buffer \right\vert \leq MAX$

• $\left\vert buffer \right\vert = 0$ inicialmente;

Comando Prova

$$\gamma_{1} \gamma_{3}$$ buffer' = buffer, e a tese de indução (P(q')) se verifica trivialmente;

$$\gamma_{2} \left\vert buffer \right\vert \leq MAX \left\vert buffer' \right\vert = \left\vert buffer \right\vert - 1 \left\vert buffer' \right\vert \leq MAX$$

$$\gamma_{4} \left\vert buffer \right\vert \leq MAX \left\vert buffer' \right\vert = \left\vert buffer \right\vert + 1 \left\vert buffer' \right\vert \gt MAX$$

E agora?