Derivação Formal de Algoritmos Distribuídos Utilizando Propriedades de Progresso - Di Iorio, Vladimir O.; Carvalho, Osvaldo S. F. (Anais do International Symposium on Computer Architecture and High Performance Computing (SBAC-PAD); 1995: Anais do VII Simpósio Brasileiro de Arquitetura de Computadores e Processamento de Alto Desempenho, 1995)
Uma estrutura de dados distribuída possui n componentes, uma em cada sítio de um sistema distribuído (nós de uma rede de computadores). A correção de uma estrutura de dados distribuída é freqüentemente expressa através de um predicado que deve ser mantido invariante. Uma técnica formal para derivação de estruturas de dados distribuídas especificada por um invariante é descrita, cuja correção é definida por um predicado global. Utilizando uma rede com dois nós, mostramos que qualquer predicado é equivalente a uma desigualdade sobre um domínio parcialmente ordenado adequadamente escolhido. O modelo é aplicado a um meio de comunicação onde as mensagens podem ser perdidas ou duplicadas, mas a ordem de envio é preservada. São derivados algoritmos para solucionar problemas entre dois nós em um meio como esse, utilizando um formato mínimo para as mensagens trocadas entre os nós.