Propriedades de invariância e de progresso

Safety (invariance) assertions : uma coisa ruim nunca acontece
- se o programa termina, seus resultados estão corretos
- o número de lugares reservados num vôo é menor ou igual ao total de assentos no avião (sem ``over-booking'')
- não existem impasses (``deadlocks'')
Progress (liveness) assertions : uma coisa boa sempre acontece
- um programa sempre termina
- toda demanda é satisfeita num tempo finito