Rotate and Double

Abstract

The program developed in this paper solves the problem of finding numbers X such that 2X = Y, where Y is derived from X by right-rotating X one digit position so that the rightmost digit becomes the leftmost digit. The problem is particularly interesting because it has vastly different solutions for number systems other than the decimal system. The developed program has the characteristic that, while it is not difficult to design, it requires a non-trivial proof of termination. This makes the development a nice candidate for demonstrating the merit of Dijkstra’s “separation of concerns.” Once termination is proven, we gain so much insight into the program that it can be substantially improved. Finally, analysis of the “useful” solutions leads to another version and an even more significant improvement in performance.

Copyright © A. N. Habermann This work was supported in part by the ZTE division of Siemens Corporation, Munich, Germany and by a grant from Westinghouse Corporation, Pattsburgh, Pennsylvania.