大多數的分散式演算法（Distributed Algorithms）沒有正式的證明（Formal proof
），一方面因為不容易想出好的證明方法，一方面因為缺乏好的證明工具，本篇論文
針對第二點提出一種新的證明符號（Proof Notation）用來幫助我們發展正式的證明
。
當我們在設計演算法時，若是站在抽象的層次（Abstract Level），則演算法只是一
些性質（Properties ）；若是站在操作的層次（Operational Level），則演算法是
可被執行的演算法則（Algorithm Rules ），所以在證明演算法時，用在抽象層次的
證明工具要能夠描述性質及作性質的推導；而用在操作層次的證明工具還要能夠描述
演算法則及作演算法則的推導。
我們所提出的證明符號主要是用在操作層次上，它對於分散式計算（Distributed C-
omputations）中所出現的性質及事件（Events ）能夠明確地描述它們的時間，列如
｛ P｝ 表示性質p 在時間u 和時間v 之間一直成立，而｛ p ｝ 表示p 在u 和v
之間某些時間成立，又如E （ P１：R ： P２）表示一個在時間u 和時間v 之間的
某個時間所發生的事件，這個事件的發生是由於應用了R 這個演算法則，而性質 P１
和性質 P２分別在此事件發生前後成立。
為了對性質作推導，我們提出了一有套有關性質及其時間的公設（Axioms）或推導法
則（Derivative Rules），用它們來進行性質的推導，而對於事件的推導，我們則應
用對演算法則的觀察所得到的一些觀察法則（Observing Rules ）來進行事件的推導
。
有一種己被廣泛使用的證明工具Temporal Logic，它主要用在抽象層次的證明上，它
提供了一些符號用來描述較抽象的性質，例如Gp表示性質 p從今以後都會成立；Fp表
示性質 p往後某些時間會成立……等等，比較起來，我們所提出的證明符號對事件及
較複雜的性質能夠作明確的描述，因此較適用於操作層次的證明，並且它也能適用在
抽象層次上。
|