The evolution of list-copying algorithms and the need for structured program verification

ABSTRACT

How can one organize the understanding of complex algorithms? People have been thinking about this issue at least since Euclid first tried to explain his innovative greatest common divisor algorithm to his colleagues, but for current research into verifying state-of-the-art programs, some precise answers to the question are needed. Over the past decade the various verification methods which have been introduced (inductive assertions, structural induction, least-fixedpoint semantics, etc.) have established many basic principles of program verification (which we define as: establishing that a program text satisfies a given pair of input-output specifications). However, it is no coincidence that most published examples of the application of these methods have dealt with "toy programs" of carefully considered simplicity.Experience indicates that these "first generation" principles, with which one can easily verify a three-line greatest common divisor algorithm, do not directly enable one to verify a 10,000 line operating system (or even a 50 line list-processing algorithm) in complete detail. To verify complex programs, additional techniques of organization, analysis and manipulation are required. (That a similar situation exists in the writing of large, correct programs has long been recognized -- structured programming being one solution.)This paper examines the usefulness of correctness-preserving program transformations (see [6]) in structuring fairly complex correctness proofs. Using our approach one starts with a simple, high-level (or "abstract") algorithm which can be easily verified, then successively refines it by implementing the abstractions of the initial algorithm to obtain various final, detailed algorithms. In Section 2 we introduce the technique by deriving the Deutsch-Schorr-Waite list-marking algorithm [14]. Our main example is the more complex problem of verifying bounded-workspace list-copying algorithms: Section 3 defines the issues, Section 4 presents the key intermediate algorithm in detail and Section 5 considers three of the most complex (published) implementations of list-copying, one of which is discussed in detail. In Section 6 we make some general remarks on program verification and the relevance of our results to the (larger) field of program correctness; Section 7 mentions some related work.

REFERENCES

• 1: Blikle, A. Towards Mathematical Structured Programming, in Formal Descriptions of Programming Concepts, E. J. Neuhold (ed.), North-Holland Publishing Co., 1978.
• 2: R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
• 3: Douglas W. Clark, A fast algorithm for copying list structures, Communications of the ACM, v.21 n.5, p.351-357, May 1978 [doi>10.1145/359488.359491]
• 4: Dijkstra, E. W. Finding the Correctness Proof of a Concurrent Program. Proc. Koninklijke Nederlandse Akademie van Wetenschappen, Amsterdam, A 81 (June 9, 1978), pp. 207-15.
• 5: David A. Fisher, Copying cyclic list structures in linear time using bounded workspace, Communications of the ACM, v.18 n.5, p.251-252, May 1975 [doi>10.1145/360762.360764]
• 6: Susan L. Gerhart, Correctness-preserving program transformations, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.54-66, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512983]
• 7: Gerhart, S. L. Proof Theory of Partial Correctness Verification Systems. SIAM J. Comp. 5 (Sept. 1976), pp. 355-77.
• 8: Gerhart, S. L. Two Proof Techniques for Transferral of Program Correctness, (forthcoming).
• 9: Susan L. Gerhart , Lawrence Yelowitz, Control structure abstractions of the backtracking programming technique, Proceedings of the 2nd international conference on Software engineering, p.391, October 13-15, 1976, San Francisco, California, United States
• 10: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 11: J. M. Robson, A bounded storage algorithm for copying cyclic structures, Communications of the ACM, v.20 n.6, p.431-433, June 1977 [doi>10.1145/359605.359628]
• 12: Willem P. de Roever, On Backtracking and Greatest Fixpoints, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.412-429, July 18-22, 1977
• 13: deRoever, W. P. An Essay on Trees and Iteration. Report RUU-CS-78-6, Dept. of Comp. Sci., University of Utrecht, 1978.
• 14: H. Schorr , W. M. Waite, An efficient machine-independent procedure for garbage collection in various list structures, Communications of the ACM, v.10 n.8, p.501-506, Aug. 1967 [doi>10.1145/363534.363554]
• 15: Topor, R. Correctness of the Schorr-Waite List Marking Algorithm. Memo MIP-R-104, School of Artificial Intelligence, Univ. of Edinburgh, 1974.
• 16: Lawrence Yelowitz , Arthur G. Duncan, Abstractions, instantiations, and proofs of marking algorithms, Proceedings of the 1977 symposium on Artificial intelligence and programming languages, p.13-21, August 15-17, 1977