UFMG - Pós-graduação em Ciência da
Computação -
Programação Paralela
A seguir: Motivação
Acima: Aula 11 - Modelos
Anterior: Aula 11 - Modelos
- 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
Osvaldo Carvalho