- - - - CENAPAD-MGCO

A seguir: Buffer: invariância de Acima: Invariantes Anterior: Prova de Invariância

Buffer: invariância de $P \equiv 0 \leq n \leq MAX$

• Claramente P(q₀) = true, pois n=0 inicialmente;
• É preciso agora varrer todos os comandos guardados, mostrando para cada um deles que se P for válido, e se a guarda do comando for válida, o estado resultante q' também obedecerá P.

Comando Prova

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

$$\gamma_{2} 0 \leq n \leq MAX 0 \leq n' \leq MAX$$

$$\gamma_{4} 0 \leq n \leq MAX 0 \leq n' \leq MAX$$