Modelos Formais: Conclusões

Modelos formais nos permitem discursar com precisão sobre as propriedades de um programa paralelo
A prova de uma propriedade nos leva a um conhecimento detalhado de um algoritmo
Modelos formais devem ser usados com sensatez: propriedades óbvias devem ser formuladas e tomadas como verdadeiras, e propriedades não óbvias merecem o esforço da prova.
Ter em mente o conjunto de propriedades expressas formalmente ao criar um algoritmo é uma enorme vantagem, como veremos mais tarde.