-
-
-
-
CENAPAD-MGCO
A seguir: Motivação
Acima: Modelos Formais para Programas
Anterior: Modelos Formais para Programas
- 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
-
Postscript -
Comentários?