- - - - CENAPAD-MGCO

A seguir: Prova de Invariância Acima: Modelos Formais para Programas Anterior: Buffer: Uma computação

Invariantes

• Um predicado de estado é uma função

  $$P: Q \rightarrow \{true, false\}$$

• Um invariante de uma computação é um predicado de estado que é válido em todos os seus estados;
• Um invariante de um sistema de transições é um invariante de todas as suas computações.