Deriving Algorithms by Adding and Removing Variables

摘要

A simple method of deriving algorithms and showing the correctness of the derivation is described. It is based on decomposing global transformations amounting to changes of representation into a number of local transformations, the correctness of which is self evident. The effectiveness of the method is demonstrated in a derivation and proof of correctness of the Deutsh-Schorr-Waite marking algorithm.