Propriedades Formais

Abordagem da Lógica Temporal :
- transformar um algoritmo em um objeto matemático formal
- expressar e provar formalmente propriedades destes objetos
Inconveniente : distância entre o objeto formal e o algoritmo real (a diminuição desta distância é um objetivo fundamental do projeto de linguagens de programação paralela, e deve sempre fazer parte das preocupações do programador)
Vantagens :
- expressão e prova de propriedades sem ambiguidades
- possibilidade de automação da verificação
Objeto formal:
- conjuntos de estados
- transições de estado
- espaço de computações
As propriedades de um algoritmo são as propriedades de seu espaço de computações