-
-
-
-
CENAPAD-MGCO
A seguir: Transações e o Protocolo
Acima: Produtor e Consumidor
Anterior: Buffer Limitado: Progresso
- 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.
Osvaldo Carvalho
-
Postscript -
Comentários?