UFMG - Pós-graduação em Ciência da
Computação -
Programação Paralela
A seguir: Sistemas de Transições de
Acima: O Buffer Compartilhado
Anterior: Propriedades do Buffer Compartilhado
- 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 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
Osvaldo Carvalho