This paper presents a relatively simple proof of a nontrivial algorithm for marking all the nodes of a list structure. The proof separates properties of the algorithm from properties of the data on which it operates and is a significant application of the method of “intermittent assertions”.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Burstall, R.M.: Proving properties of programs by structural induction. Comput. J. 12, 41–48 (1969)
Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. In: Machine intelligence, Vol. 7 (B. Meltzer, D. Michie, eds.), pp. 23–50. Edinburgh: University Press 1972
Burstall, R.M.: Program proving as hand simulation with a little induction. In: Proc. IFIP Congress 1974, pp. 308–312. Amsterdam: North-Holland 1974
Floyd, R.W.: Assigning meanings to programs. In: Proc. Symposium in Applied Mathematics 19 (J.T. Schwartz, ed.), pp. 19–32. Providence, R.I.: AMS 1967
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informat. 1, 271–281 (1972)
Knuth, D.W.: The art of computer programming, Vol. 1. Fundamental algorithms. Reading, Mass.: Addison-Wesley 1968
Kowaltowski, T.: Correctness of programs manipulating data structures. Ph.D. thesis, University of California, Berkeley, 1973
Manna, Z., Waldinger, R.: Is “sometime” sometimes better than “always”? Intermittent assertions in proving program correctness. Comm. ACM 21, 159–172 (1978)
Milner, R.: An algebraic definition of simulation between programs. Report No. CS-205, Computer Science Department, Stanford University, 1971
Morris, J.H. Jr.: Verification-oriented language design. Technical Report 7, Department of Computer Science, University of California, Berkeley, 1972
Poupon, J., Wegbreit, B.: Covering functions. Unpublished report, Centre for Research in Computing Technology, Harvard University, 1972
Schorr, H., Waite, W.M.: An efficient machine-independent procedure for garbage collection in various list structures. Comm. ACM 10, 501–506 (1967)
Scott, D.: Outline of a mathematical theory of computation. Proc. 4th Annual Princeton Conference on Information Sciences and Systems, pp. 169–176, 1970
Suzuki: Automatic verification of programs with complex data structures. Ph.D. thesis, Stanford University, 1976
Gries, D.: The Schorr-Waite graph marking algorithm. Acta Informat. 11, 223–232 (1979)
(This paper grew out of an earlier version which was submitted to this journal on October 16, 1974)
About this article
Cite this article
Topor, R.W. The correctness of the Schorr-Waite list marking algorithm. Acta Informatica 11, 211–221 (1979). https://doi.org/10.1007/BF00289067
- Information System
- Operating System
- Data Structure
- Communication Network
- Information Theory