Formal Design Method For Reasoning about Algorithms and Representing Efficient Programs