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

A seguir: Prova de Invariância Acima: Aula 11 - Modelos Anterior: Buffer: Uma computação

Invariantes

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.